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

Theorem ifbothda 3812
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 3785 . . . . . 6  |-  ( ph  ->  if ( ph ,  A ,  B )  =  A )
32eqcomd 2438 . . . . 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 463 . . 3  |-  ( ( et  /\  ph )  ->  ( ps  <->  th )
)
71, 6mpbid 210 . 2  |-  ( ( et  /\  ph )  ->  th )
8 ifbothda.4 . . 3  |-  ( ( et  /\  -.  ph )  ->  ch )
9 iffalse 3787 . . . . . 6  |-  ( -. 
ph  ->  if ( ph ,  A ,  B )  =  B )
109eqcomd 2438 . . . . 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 463 . . 3  |-  ( ( et  /\  -.  ph )  ->  ( ch  <->  th )
)
148, 13mpbid 210 . 2  |-  ( ( et  /\  -.  ph )  ->  th )
157, 14pm2.61dan 782 1  |-  ( et 
->  th )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1362   ifcif 3779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-if 3780
This theorem is referenced by:  ifboth  3813  resixpfo  7289  boxriin  7293  boxcutc  7294  suppr  7706  cantnflem1  7885  cantnfp1OLD  7903  cantnflem1OLD  7908  ttukeylem5  8670  ttukeylem6  8671  ccatco  12447  bitsinv1lem  13620  bitsinv1  13621  bitsinvp1  13628  smumullem  13671  ramcl2lem  14053  acsfn  14580  tsrlemax  15373  odlem1  16018  gexlem1  16058  cyggex2  16353  dprdfeq0  16486  dprdfeq0OLD  16493  mplmon2  17507  coe1tmmul2  17627  coe1tmmul  17628  xrsdsreval  17702  xrsdsreclb  17704  ptcld  19028  xkopt  19070  stdbdxmet  19932  xrsxmet  20228  iccpnfcnv  20358  iccpnfhmeo  20359  xrhmeo  20360  oprpiece1res2  20366  phtpycc  20405  dvcobr  21262  evlslem1  21367  mdegle0  21433  dvradcnv  21771  psercnlem1  21775  psercn  21776  logtayl  21990  atantayl2  22218  efrlim  22248  musum  22416  dchrmulid2  22476  dchrsum2  22492  sumdchr2  22494  dchrisum0flblem1  22642  dchrisum0flblem2  22643  rplogsum  22661  pntlemj  22737  eupath2lem1  23421  eupath  23425  ifeqeqx  25726  xrge0iifcnv  26217  xrge0iifhom  26221  esumpinfval  26376  dstfrvunirn  26705  sgn3da  26772  ccatmulgnn0dir  26788  plymulx0  26796  plymulx  26797  signswmnd  26806  signswn0  26809  signswch  26810  lgamgulmlem5  26867  cnambfre  28284  itg2addnclem  28287  itg2addnclem3  28289  itg2addnc  28290  itg2gt0cn  28291  ftc1anclem7  28317  ftc1anclem8  28318  ftc1anc  28319  fnejoin2  28434  kelac1  29261  hashgcdeq  29411
  Copyright terms: Public domain W3C validator