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

Theorem ifboth 3981
Description: A wff  th containing a conditional operator is true when both of its cases are true. (Contributed by NM, 3-Sep-2006.) (Revised by Mario Carneiro, 15-Feb-2015.)
Hypotheses
Ref Expression
ifboth.1  |-  ( A  =  if ( ph ,  A ,  B )  ->  ( ps  <->  th )
)
ifboth.2  |-  ( B  =  if ( ph ,  A ,  B )  ->  ( ch  <->  th )
)
Assertion
Ref Expression
ifboth  |-  ( ( ps  /\  ch )  ->  th )

Proof of Theorem ifboth
StepHypRef Expression
1 ifboth.1 . 2  |-  ( A  =  if ( ph ,  A ,  B )  ->  ( ps  <->  th )
)
2 ifboth.2 . 2  |-  ( B  =  if ( ph ,  A ,  B )  ->  ( ch  <->  th )
)
3 simpll 753 . 2  |-  ( ( ( ps  /\  ch )  /\  ph )  ->  ps )
4 simplr 754 . 2  |-  ( ( ( ps  /\  ch )  /\  -.  ph )  ->  ch )
51, 2, 3, 4ifbothda 3980 1  |-  ( ( ps  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1379   ifcif 3945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-if 3946
This theorem is referenced by:  ifcl  3987  keephyp  4010  soltmin  5412  xrmaxlt  11394  xrltmin  11395  xrmaxle  11396  xrlemin  11397  ifle  11408  expmulnbnd  12278  limsupgre  13284  isumless  13637  cvgrat  13672  rpnnen2lem4  13829  ruclem2  13843  sadcaddlem  13983  sadadd3  13987  pcmptdvds  14289  prmreclem5  14314  prmreclem6  14315  pnfnei  19589  mnfnei  19590  xkopt  20024  xmetrtri2  20727  stdbdxmet  20886  stdbdmet  20887  stdbdmopn  20889  xrsxmet  21182  icccmplem2  21196  metdscn  21228  metnrmlem1a  21230  ivthlem2  21732  ovolicc2lem5  21800  ioombl1lem1  21836  ioombl1lem4  21839  ismbfd  21915  mbfi1fseqlem4  21993  mbfi1fseqlem5  21994  itg2const  22015  itg2const2  22016  itg2monolem3  22027  itg2gt0  22035  itg2cnlem1  22036  itg2cnlem2  22037  iblss  22079  itgless  22091  ibladdlem  22094  iblabsr  22104  iblmulc2  22105  dvferm1lem  22253  dvferm2lem  22255  dvlip2  22264  dgradd2  22532  plydiveu  22561  chtppilim  23526  dchrvmasumiflem1  23552  ostth3  23689  mblfinlem2  29979  itg2addnclem  29993  itg2addnc  29996  itg2gt0cn  29997  ibladdnclem  29998  iblmulc2nc  30007  bddiblnc  30012  ftc1anclem5  30021  ftc1anclem8  30024  ftc1anc  30025
  Copyright terms: Public domain W3C validator