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

Theorem ifbothda 3819
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 3792 . . . . . 6  |-  ( ph  ->  if ( ph ,  A ,  B )  =  A )
32eqcomd 2443 . . . . 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 3794 . . . . . 6  |-  ( -. 
ph  ->  if ( ph ,  A ,  B )  =  B )
109eqcomd 2443 . . . . 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 1369   ifcif 3786
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-if 3787
This theorem is referenced by:  ifboth  3820  resixpfo  7293  boxriin  7297  boxcutc  7298  suppr  7710  cantnflem1  7889  cantnfp1OLD  7907  cantnflem1OLD  7912  ttukeylem5  8674  ttukeylem6  8675  ccatco  12455  bitsinv1lem  13629  bitsinv1  13630  bitsinvp1  13637  smumullem  13680  ramcl2lem  14062  acsfn  14589  tsrlemax  15382  odlem1  16029  gexlem1  16069  cyggex2  16364  dprdfeq0  16500  dprdfeq0OLD  16507  mplmon2  17550  evlslem1  17576  coe1tmmul2  17704  coe1tmmul  17705  xrsdsreval  17833  xrsdsreclb  17835  ptcld  19161  xkopt  19203  stdbdxmet  20065  xrsxmet  20361  iccpnfcnv  20491  iccpnfhmeo  20492  xrhmeo  20493  oprpiece1res2  20499  phtpycc  20538  dvcobr  21395  mdegle0  21523  dvradcnv  21861  psercnlem1  21865  psercn  21866  logtayl  22080  atantayl2  22308  efrlim  22338  musum  22506  dchrmulid2  22566  dchrsum2  22582  sumdchr2  22584  dchrisum0flblem1  22732  dchrisum0flblem2  22733  rplogsum  22751  pntlemj  22827  eupath2lem1  23549  eupath  23553  ifeqeqx  25853  xrge0iifcnv  26315  xrge0iifhom  26319  esumpinfval  26474  dstfrvunirn  26809  sgn3da  26876  ccatmulgnn0dir  26892  plymulx0  26900  plymulx  26901  signswmnd  26910  signswn0  26913  signswch  26914  lgamgulmlem5  26971  cnambfre  28393  itg2addnclem  28396  itg2addnclem3  28398  itg2addnc  28399  itg2gt0cn  28400  ftc1anclem7  28426  ftc1anclem8  28427  ftc1anc  28428  fnejoin2  28543  kelac1  29369  hashgcdeq  29519
  Copyright terms: Public domain W3C validator