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

Theorem ifbothda 3769
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 3745 . . . . . 6  |-  ( ph  ->  if ( ph ,  A ,  B )  =  A )
32eqcomd 2441 . . . . 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 453 . . 3  |-  ( ( et  /\  ph )  ->  ( ps  <->  th )
)
71, 6mpbid 202 . 2  |-  ( ( et  /\  ph )  ->  th )
8 ifbothda.4 . . 3  |-  ( ( et  /\  -.  ph )  ->  ch )
9 iffalse 3746 . . . . . 6  |-  ( -. 
ph  ->  if ( ph ,  A ,  B )  =  B )
109eqcomd 2441 . . . . 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 453 . . 3  |-  ( ( et  /\  -.  ph )  ->  ( ch  <->  th )
)
148, 13mpbid 202 . 2  |-  ( ( et  /\  -.  ph )  ->  th )
157, 14pm2.61dan 767 1  |-  ( et 
->  th )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1652   ifcif 3739
This theorem is referenced by:  ifboth  3770  resixpfo  7100  boxriin  7104  boxcutc  7105  suppr  7473  cantnfp1  7637  cantnflem1  7645  ttukeylem5  8393  ttukeylem6  8394  ccatco  11804  bitsinv1lem  12953  bitsinv1  12954  bitsinvp1  12961  smumullem  13004  ramcl2lem  13377  acsfn  13884  tsrlemax  14652  odlem1  15173  gexlem1  15213  cyggex2  15506  dprdfeq0  15580  mplmon2  16553  coe1tmmul2  16668  coe1tmmul  16669  xrsdsreval  16743  xrsdsreclb  16745  ptcld  17645  xkopt  17687  stdbdxmet  18545  xrsxmet  18840  iccpnfcnv  18969  iccpnfhmeo  18970  xrhmeo  18971  oprpiece1res2  18977  phtpycc  19016  dvcobr  19832  evlslem1  19936  mdegle0  20000  dvradcnv  20337  psercnlem1  20341  psercn  20342  logtayl  20551  atantayl2  20778  efrlim  20808  musum  20976  dchrmulid2  21036  dchrsum2  21052  sumdchr2  21054  dchrisum0flblem1  21202  dchrisum0flblem2  21203  rplogsum  21221  pntlemj  21297  eupath2lem1  21699  eupath  21703  ifeqeqx  24001  xrge0iifcnv  24319  xrge0iifhom  24323  esumpinfval  24463  dstfrvunirn  24732  lgamgulmlem5  24817  cnambfre  26255  itg2addnclem  26256  itg2addnclem3  26258  itg2addnc  26259  itg2gt0cn  26260  ftc1anclem7  26286  ftc1anclem8  26287  ftc1anc  26288  fnejoin2  26398  kelac1  27138  hashgcdeq  27494
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-if 3740
  Copyright terms: Public domain W3C validator