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

Theorem ifboth 3945
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 758 . 2  |-  ( ( ( ps  /\  ch )  /\  ph )  ->  ps )
4 simplr 760 . 2  |-  ( ( ( ps  /\  ch )  /\  -.  ph )  ->  ch )
51, 2, 3, 4ifbothda 3944 1  |-  ( ( ps  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    /\ wa 370    = wceq 1437   ifcif 3909
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-if 3910
This theorem is referenced by:  ifcl  3951  keephyp  3973  soltmin  5251  xrmaxlt  11476  xrltmin  11477  xrmaxle  11478  xrlemin  11479  ifle  11490  expmulnbnd  12403  limsupgre  13529  limsupgreOLD  13530  isumless  13890  cvgrat  13926  rpnnen2lem4  14257  ruclem2  14271  sadcaddlem  14418  sadadd3  14422  pcmptdvds  14826  prmreclem5  14851  prmreclem6  14852  pnfnei  20222  mnfnei  20223  xkopt  20656  xmetrtri2  21357  stdbdxmet  21516  stdbdmet  21517  stdbdmopn  21519  xrsxmet  21813  icccmplem2  21827  metdscn  21859  metnrmlem1a  21861  metdscnOLD  21874  metnrmlem1aOLD  21876  ivthlem2  22389  ovolicc2lem5  22461  ioombl1lem1  22497  ioombl1lem4  22500  ismbfd  22582  mbfi1fseqlem4  22662  mbfi1fseqlem5  22663  itg2const  22684  itg2const2  22685  itg2monolem3  22696  itg2gt0  22704  itg2cnlem1  22705  itg2cnlem2  22706  iblss  22748  itgless  22760  ibladdlem  22763  iblabsr  22773  iblmulc2  22774  dvferm1lem  22922  dvferm2lem  22924  dvlip2  22933  dgradd2  23208  plydiveu  23237  chtppilim  24299  dchrvmasumiflem1  24325  ostth3  24462  1smat1  28625  poimirlem24  31877  mblfinlem2  31891  itg2addnclem  31906  itg2addnc  31909  itg2gt0cn  31910  ibladdnclem  31911  iblmulc2nc  31920  bddiblnc  31925  ftc1anclem5  31934  ftc1anclem8  31937  ftc1anc  31938
  Copyright terms: Public domain W3C validator