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

Theorem ifboth 3609
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 730 . 2  |-  ( ( ( ps  /\  ch )  /\  ph )  ->  ps )
4 simplr 731 . 2  |-  ( ( ( ps  /\  ch )  /\  -.  ph )  ->  ch )
51, 2, 3, 4ifbothda 3608 1  |-  ( ( ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1632   ifcif 3578
This theorem is referenced by:  ifcl  3614  keephyp  3632  soltmin  5098  xrmaxlt  10526  xrltmin  10527  xrmaxle  10528  xrlemin  10529  ifle  10540  expmulnbnd  11249  limsupgre  11971  isumless  12320  cvgrat  12355  rpnnen2lem4  12512  ruclem2  12526  sadcaddlem  12664  sadadd3  12668  pcmptdvds  12958  prmreclem5  12983  prmreclem6  12984  pnfnei  16966  mnfnei  16967  xkopt  17365  xmetrtri2  17936  stdbdxmet  18077  stdbdmet  18078  stdbdmopn  18080  xrsxmet  18331  icccmplem2  18344  metdscn  18376  metnrmlem1a  18378  ivthlem2  18828  ovolicc2lem5  18896  ioombl1lem1  18931  ioombl1lem4  18934  ismbfd  19011  mbfi1fseqlem4  19089  mbfi1fseqlem5  19090  itg2const  19111  itg2const2  19112  itg2monolem3  19123  itg2gt0  19131  itg2cnlem1  19132  itg2cnlem2  19133  iblss  19175  itgless  19187  ibladdlem  19190  iblabsr  19200  iblmulc2  19201  dvferm1lem  19347  dvferm2lem  19349  dvlip2  19358  dgradd2  19665  plydiveu  19694  chtppilim  20640  dchrvmasumiflem1  20666  ostth3  20803  itg2addnclem  25003  itg2addnc  25005  itg2gt0cn  25006  ibladdnclem  25007  iblmulc2nc  25016  bddiblnc  25021
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-if 3579
  Copyright terms: Public domain W3C validator