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

Theorem ifbothda 3961
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 3932 . . . . . 6  |-  ( ph  ->  if ( ph ,  A ,  B )  =  A )
32eqcomd 2451 . . . . 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 3935 . . . . . 6  |-  ( -. 
ph  ->  if ( ph ,  A ,  B )  =  B )
109eqcomd 2451 . . . . 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 791 1  |-  ( et 
->  th )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1383   ifcif 3926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-if 3927
This theorem is referenced by:  ifboth  3962  resixpfo  7509  boxriin  7513  boxcutc  7514  suppr  7932  cantnflem1  8111  cantnfp1OLD  8129  cantnflem1OLD  8134  ttukeylem5  8896  ttukeylem6  8897  bitsinv1lem  14073  bitsinv1  14074  smumullem  14124  ramcl2lem  14509  acsfn  15038  tsrlemax  15829  odlem1  16538  gexlem1  16578  cyggex2  16878  dprdfeq0  17041  dprdfeq0OLD  17048  mplmon2  18137  evlslem1  18163  coe1tmmul2  18296  coe1tmmul  18297  xrsdsreclb  18444  ptcld  20092  xkopt  20134  stdbdxmet  20996  xrsxmet  21292  iccpnfcnv  21422  iccpnfhmeo  21423  xrhmeo  21424  dvcobr  22327  mdegle0  22455  dvradcnv  22794  psercnlem1  22798  psercn  22799  logtayl  23019  efrlim  23277  musum  23445  dchrmulid2  23505  dchrsum2  23521  sumdchr2  23523  dchrisum0flblem1  23671  dchrisum0flblem2  23672  rplogsum  23690  pntlemj  23766  eupath2lem1  24955  eupath  24959  ifeqeqx  27397  xrge0iifcnv  27893  xrge0iifhom  27897  esumpinfval  28057  dstfrvunirn  28391  sgn3da  28458  plymulx0  28482  signswn0  28495  signswch  28496  lgamgulmlem5  28553  cnambfre  30039  itg2addnclem  30042  itg2addnclem3  30044  itg2addnc  30045  itg2gt0cn  30046  ftc1anclem7  30072  ftc1anclem8  30073  ftc1anc  30074  fnejoin2  30163  kelac1  30985  hashgcdeq  31134
  Copyright terms: Public domain W3C validator