MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ifbothda Unicode version

Theorem ifbothda 3595
Description: A wff  th containing a conditional operator is true when both of its cases are true. (Contributed by NM, 15-Feb-2015.)
Hypotheses
Ref Expression
ifboth.1  |-  ( A  =  if ( ph ,  A ,  B )  ->  ( ps  <->  th )
)
ifboth.2  |-  ( B  =  if ( ph ,  A ,  B )  ->  ( ch  <->  th )
)
ifbothda.3  |-  ( ( et  /\  ph )  ->  ps )
ifbothda.4  |-  ( ( et  /\  -.  ph )  ->  ch )
Assertion
Ref Expression
ifbothda  |-  ( et 
->  th )

Proof of Theorem ifbothda
StepHypRef Expression
1 ifbothda.3 . . 3  |-  ( ( et  /\  ph )  ->  ps )
2 iftrue 3571 . . . . . 6  |-  ( ph  ->  if ( ph ,  A ,  B )  =  A )
32eqcomd 2288 . . . . 5  |-  ( ph  ->  A  =  if (
ph ,  A ,  B ) )
4 ifboth.1 . . . . 5  |-  ( A  =  if ( ph ,  A ,  B )  ->  ( ps  <->  th )
)
53, 4syl 15 . . . 4  |-  ( ph  ->  ( ps  <->  th )
)
65adantl 452 . . 3  |-  ( ( et  /\  ph )  ->  ( ps  <->  th )
)
71, 6mpbid 201 . 2  |-  ( ( et  /\  ph )  ->  th )
8 ifbothda.4 . . 3  |-  ( ( et  /\  -.  ph )  ->  ch )
9 iffalse 3572 . . . . . 6  |-  ( -. 
ph  ->  if ( ph ,  A ,  B )  =  B )
109eqcomd 2288 . . . . 5  |-  ( -. 
ph  ->  B  =  if ( ph ,  A ,  B ) )
11 ifboth.2 . . . . 5  |-  ( B  =  if ( ph ,  A ,  B )  ->  ( ch  <->  th )
)
1210, 11syl 15 . . . 4  |-  ( -. 
ph  ->  ( ch  <->  th )
)
1312adantl 452 . . 3  |-  ( ( et  /\  -.  ph )  ->  ( ch  <->  th )
)
148, 13mpbid 201 . 2  |-  ( ( et  /\  -.  ph )  ->  th )
157, 14pm2.61dan 766 1  |-  ( et 
->  th )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1623   ifcif 3565
This theorem is referenced by:  ifboth  3596  resixpfo  6854  boxriin  6858  boxcutc  6859  suppr  7219  cantnfp1  7383  cantnflem1  7391  ttukeylem5  8140  ttukeylem6  8141  ccatco  11490  bitsinv1lem  12632  bitsinv1  12633  bitsinvp1  12640  smumullem  12683  ramcl2lem  13056  acsfn  13561  tsrlemax  14329  odlem1  14850  gexlem1  14890  cyggex2  15183  dprdfeq0  15257  mplmon2  16234  coe1tmmul2  16352  coe1tmmul  16353  xrsdsreval  16416  xrsdsreclb  16418  ptcld  17307  xkopt  17349  stdbdxmet  18061  xrsxmet  18315  iccpnfcnv  18442  iccpnfhmeo  18443  xrhmeo  18444  oprpiece1res2  18450  phtpycc  18489  dvcobr  19295  evlslem1  19399  mdegle0  19463  dvradcnv  19797  psercnlem1  19801  psercn  19802  logtayl  20007  atantayl2  20234  efrlim  20264  musum  20431  dchrmulid2  20491  dchrsum2  20507  sumdchr2  20509  dchrisum0flblem1  20657  dchrisum0flblem2  20658  rplogsum  20676  pntlemj  20752  ifeqeqx  23034  xrge0iifcnv  23315  xrge0iifhom  23319  esumpinfval  23441  dstfrvunirn  23675  eupath2lem1  23901  eupath  23905  fnejoin2  26318  kelac1  27161  hashgcdeq  27517
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-if 3566
  Copyright terms: Public domain W3C validator