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

Theorem ifboth 3730
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 731 . 2  |-  ( ( ( ps  /\  ch )  /\  ph )  ->  ps )
4 simplr 732 . 2  |-  ( ( ( ps  /\  ch )  /\  -.  ph )  ->  ch )
51, 2, 3, 4ifbothda 3729 1  |-  ( ( ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1649   ifcif 3699
This theorem is referenced by:  ifcl  3735  keephyp  3753  soltmin  5232  xrmaxlt  10725  xrltmin  10726  xrmaxle  10727  xrlemin  10728  ifle  10739  expmulnbnd  11466  limsupgre  12230  isumless  12580  cvgrat  12615  rpnnen2lem4  12772  ruclem2  12786  sadcaddlem  12924  sadadd3  12928  pcmptdvds  13218  prmreclem5  13243  prmreclem6  13244  pnfnei  17238  mnfnei  17239  xkopt  17640  xmetrtri2  18339  stdbdxmet  18498  stdbdmet  18499  stdbdmopn  18501  xrsxmet  18793  icccmplem2  18807  metdscn  18839  metnrmlem1a  18841  ivthlem2  19302  ovolicc2lem5  19370  ioombl1lem1  19405  ioombl1lem4  19408  ismbfd  19485  mbfi1fseqlem4  19563  mbfi1fseqlem5  19564  itg2const  19585  itg2const2  19586  itg2monolem3  19597  itg2gt0  19605  itg2cnlem1  19606  itg2cnlem2  19607  iblss  19649  itgless  19661  ibladdlem  19664  iblabsr  19674  iblmulc2  19675  dvferm1lem  19821  dvferm2lem  19823  dvlip2  19832  dgradd2  20139  plydiveu  20168  chtppilim  21122  dchrvmasumiflem1  21148  ostth3  21285  mblfinlem  26143  itg2addnclem  26155  itg2addnc  26158  itg2gt0cn  26159  ibladdnclem  26160  iblmulc2nc  26169  bddiblnc  26174
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-if 3700
  Copyright terms: Public domain W3C validator