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

Theorem ifboth 3596
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 3595 1  |-  ( ( ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1623   ifcif 3565
This theorem is referenced by:  ifcl  3601  keephyp  3619  soltmin  5082  xrmaxlt  10510  xrltmin  10511  xrmaxle  10512  xrlemin  10513  ifle  10524  expmulnbnd  11233  limsupgre  11955  isumless  12304  cvgrat  12339  rpnnen2lem4  12496  ruclem2  12510  sadcaddlem  12648  sadadd3  12652  pcmptdvds  12942  prmreclem5  12967  prmreclem6  12968  pnfnei  16950  mnfnei  16951  xkopt  17349  xmetrtri2  17920  stdbdxmet  18061  stdbdmet  18062  stdbdmopn  18064  xrsxmet  18315  icccmplem2  18328  metdscn  18360  metnrmlem1a  18362  ivthlem2  18812  ovolicc2lem5  18880  ioombl1lem1  18915  ioombl1lem4  18918  ismbfd  18995  mbfi1fseqlem4  19073  mbfi1fseqlem5  19074  itg2const  19095  itg2const2  19096  itg2monolem3  19107  itg2gt0  19115  itg2cnlem1  19116  itg2cnlem2  19117  iblss  19159  itgless  19171  ibladdlem  19174  iblabsr  19184  iblmulc2  19185  dvferm1lem  19331  dvferm2lem  19333  dvlip2  19342  dgradd2  19649  plydiveu  19678  chtppilim  20624  dchrvmasumiflem1  20650  ostth3  20787
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-if 3566
  Copyright terms: Public domain W3C validator