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

Theorem ifbothda 3729
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 3705 . . . . . 6  |-  ( ph  ->  if ( ph ,  A ,  B )  =  A )
32eqcomd 2409 . . . . 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 3706 . . . . . 6  |-  ( -. 
ph  ->  if ( ph ,  A ,  B )  =  B )
109eqcomd 2409 . . . . 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 1649   ifcif 3699
This theorem is referenced by:  ifboth  3730  resixpfo  7059  boxriin  7063  boxcutc  7064  suppr  7429  cantnfp1  7593  cantnflem1  7601  ttukeylem5  8349  ttukeylem6  8350  ccatco  11759  bitsinv1lem  12908  bitsinv1  12909  bitsinvp1  12916  smumullem  12959  ramcl2lem  13332  acsfn  13839  tsrlemax  14607  odlem1  15128  gexlem1  15168  cyggex2  15461  dprdfeq0  15535  mplmon2  16508  coe1tmmul2  16623  coe1tmmul  16624  xrsdsreval  16698  xrsdsreclb  16700  ptcld  17598  xkopt  17640  stdbdxmet  18498  xrsxmet  18793  iccpnfcnv  18922  iccpnfhmeo  18923  xrhmeo  18924  oprpiece1res2  18930  phtpycc  18969  dvcobr  19785  evlslem1  19889  mdegle0  19953  dvradcnv  20290  psercnlem1  20294  psercn  20295  logtayl  20504  atantayl2  20731  efrlim  20761  musum  20929  dchrmulid2  20989  dchrsum2  21005  sumdchr2  21007  dchrisum0flblem1  21155  dchrisum0flblem2  21156  rplogsum  21174  pntlemj  21250  eupath2lem1  21652  eupath  21656  ifeqeqx  23954  xrge0iifcnv  24272  xrge0iifhom  24276  esumpinfval  24416  dstfrvunirn  24685  lgamgulmlem5  24770  cnambfre  26154  itg2addnclem  26155  itg2addnclem3  26157  itg2addnc  26158  itg2gt0cn  26159  fnejoin2  26288  kelac1  27029  hashgcdeq  27385
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-if 3700
  Copyright terms: Public domain W3C validator