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

Theorem ifbothda 3608
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 3584 . . . . . 6  |-  ( ph  ->  if ( ph ,  A ,  B )  =  A )
32eqcomd 2301 . . . . 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 3585 . . . . . 6  |-  ( -. 
ph  ->  if ( ph ,  A ,  B )  =  B )
109eqcomd 2301 . . . . 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 1632   ifcif 3578
This theorem is referenced by:  ifboth  3609  resixpfo  6870  boxriin  6874  boxcutc  6875  suppr  7235  cantnfp1  7399  cantnflem1  7407  ttukeylem5  8156  ttukeylem6  8157  ccatco  11506  bitsinv1lem  12648  bitsinv1  12649  bitsinvp1  12656  smumullem  12699  ramcl2lem  13072  acsfn  13577  tsrlemax  14345  odlem1  14866  gexlem1  14906  cyggex2  15199  dprdfeq0  15273  mplmon2  16250  coe1tmmul2  16368  coe1tmmul  16369  xrsdsreval  16432  xrsdsreclb  16434  ptcld  17323  xkopt  17365  stdbdxmet  18077  xrsxmet  18331  iccpnfcnv  18458  iccpnfhmeo  18459  xrhmeo  18460  oprpiece1res2  18466  phtpycc  18505  dvcobr  19311  evlslem1  19415  mdegle0  19479  dvradcnv  19813  psercnlem1  19817  psercn  19818  logtayl  20023  atantayl2  20250  efrlim  20280  musum  20447  dchrmulid2  20507  dchrsum2  20523  sumdchr2  20525  dchrisum0flblem1  20673  dchrisum0flblem2  20674  rplogsum  20692  pntlemj  20768  ifeqeqx  23050  xrge0iifcnv  23330  xrge0iifhom  23334  esumpinfval  23456  dstfrvunirn  23690  eupath2lem1  23916  eupath  23920  itg2addnc  25005  itg2gt0cn  25006  fnejoin2  26421  kelac1  27264  hashgcdeq  27620
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-if 3579
  Copyright terms: Public domain W3C validator