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

Theorem ifbothda 3974
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 3945 . . . . . 6  |-  ( ph  ->  if ( ph ,  A ,  B )  =  A )
32eqcomd 2475 . . . . 5  |-  ( ph  ->  A  =  if (
ph ,  A ,  B ) )
4 ifboth.1 . . . . 5  |-  ( A  =  if ( ph ,  A ,  B )  ->  ( ps  <->  th )
)
53, 4syl 16 . . . 4  |-  ( ph  ->  ( ps  <->  th )
)
65adantl 466 . . 3  |-  ( ( et  /\  ph )  ->  ( ps  <->  th )
)
71, 6mpbid 210 . 2  |-  ( ( et  /\  ph )  ->  th )
8 ifbothda.4 . . 3  |-  ( ( et  /\  -.  ph )  ->  ch )
9 iffalse 3948 . . . . . 6  |-  ( -. 
ph  ->  if ( ph ,  A ,  B )  =  B )
109eqcomd 2475 . . . . 5  |-  ( -. 
ph  ->  B  =  if ( ph ,  A ,  B ) )
11 ifboth.2 . . . . 5  |-  ( B  =  if ( ph ,  A ,  B )  ->  ( ch  <->  th )
)
1210, 11syl 16 . . . 4  |-  ( -. 
ph  ->  ( ch  <->  th )
)
1312adantl 466 . . 3  |-  ( ( et  /\  -.  ph )  ->  ( ch  <->  th )
)
148, 13mpbid 210 . 2  |-  ( ( et  /\  -.  ph )  ->  th )
157, 14pm2.61dan 789 1  |-  ( et 
->  th )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1379   ifcif 3939
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-if 3940
This theorem is referenced by:  ifboth  3975  resixpfo  7507  boxriin  7511  boxcutc  7512  suppr  7929  cantnflem1  8108  cantnfp1OLD  8126  cantnflem1OLD  8131  ttukeylem5  8893  ttukeylem6  8894  ccatco  12764  bitsinv1lem  13950  bitsinv1  13951  bitsinvp1  13958  smumullem  14001  ramcl2lem  14386  acsfn  14914  tsrlemax  15707  odlem1  16365  gexlem1  16405  cyggex2  16702  dprdfeq0  16864  dprdfeq0OLD  16871  mplmon2  17957  evlslem1  17983  coe1tmmul2  18116  coe1tmmul  18117  xrsdsreval  18259  xrsdsreclb  18261  ptcld  19877  xkopt  19919  stdbdxmet  20781  xrsxmet  21077  iccpnfcnv  21207  iccpnfhmeo  21208  xrhmeo  21209  oprpiece1res2  21215  phtpycc  21254  dvcobr  22112  mdegle0  22240  dvradcnv  22578  psercnlem1  22582  psercn  22583  logtayl  22797  atantayl2  23025  efrlim  23055  musum  23223  dchrmulid2  23283  dchrsum2  23299  sumdchr2  23301  dchrisum0flblem1  23449  dchrisum0flblem2  23450  rplogsum  23468  pntlemj  23544  eupath2lem1  24681  eupath  24685  ifeqeqx  27121  xrge0iifcnv  27579  xrge0iifhom  27583  esumpinfval  27747  dstfrvunirn  28081  sgn3da  28148  ccatmulgnn0dir  28164  plymulx0  28172  plymulx  28173  signswmnd  28182  signswn0  28185  signswch  28186  lgamgulmlem5  28243  cnambfre  29668  itg2addnclem  29671  itg2addnclem3  29673  itg2addnc  29674  itg2gt0cn  29675  ftc1anclem7  29701  ftc1anclem8  29702  ftc1anc  29703  fnejoin2  29818  kelac1  30641  hashgcdeq  30791
  Copyright terms: Public domain W3C validator