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

Theorem ifbothda 3931
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 3904 . . . . . 6  |-  ( ph  ->  if ( ph ,  A ,  B )  =  A )
32eqcomd 2462 . . . . 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 3906 . . . . . 6  |-  ( -. 
ph  ->  if ( ph ,  A ,  B )  =  B )
109eqcomd 2462 . . . . 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 1370   ifcif 3898
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-if 3899
This theorem is referenced by:  ifboth  3932  resixpfo  7410  boxriin  7414  boxcutc  7415  suppr  7828  cantnflem1  8007  cantnfp1OLD  8025  cantnflem1OLD  8030  ttukeylem5  8792  ttukeylem6  8793  ccatco  12580  bitsinv1lem  13754  bitsinv1  13755  bitsinvp1  13762  smumullem  13805  ramcl2lem  14187  acsfn  14715  tsrlemax  15508  odlem1  16158  gexlem1  16198  cyggex2  16493  dprdfeq0  16633  dprdfeq0OLD  16640  mplmon2  17698  evlslem1  17724  coe1tmmul2  17852  coe1tmmul  17853  xrsdsreval  17982  xrsdsreclb  17984  ptcld  19317  xkopt  19359  stdbdxmet  20221  xrsxmet  20517  iccpnfcnv  20647  iccpnfhmeo  20648  xrhmeo  20649  oprpiece1res2  20655  phtpycc  20694  dvcobr  21552  mdegle0  21680  dvradcnv  22018  psercnlem1  22022  psercn  22023  logtayl  22237  atantayl2  22465  efrlim  22495  musum  22663  dchrmulid2  22723  dchrsum2  22739  sumdchr2  22741  dchrisum0flblem1  22889  dchrisum0flblem2  22890  rplogsum  22908  pntlemj  22984  eupath2lem1  23749  eupath  23753  ifeqeqx  26053  xrge0iifcnv  26507  xrge0iifhom  26511  esumpinfval  26666  dstfrvunirn  27000  sgn3da  27067  ccatmulgnn0dir  27083  plymulx0  27091  plymulx  27092  signswmnd  27101  signswn0  27104  signswch  27105  lgamgulmlem5  27162  cnambfre  28587  itg2addnclem  28590  itg2addnclem3  28592  itg2addnc  28593  itg2gt0cn  28594  ftc1anclem7  28620  ftc1anclem8  28621  ftc1anc  28622  fnejoin2  28737  kelac1  29563  hashgcdeq  29713
  Copyright terms: Public domain W3C validator