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

Theorem ifboth 3772
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 732 . 2  |-  ( ( ( ps  /\  ch )  /\  ph )  ->  ps )
4 simplr 733 . 2  |-  ( ( ( ps  /\  ch )  /\  -.  ph )  ->  ch )
51, 2, 3, 4ifbothda 3771 1  |-  ( ( ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 178    /\ wa 360    = wceq 1653   ifcif 3741
This theorem is referenced by:  ifcl  3777  keephyp  3795  soltmin  5275  xrmaxlt  10771  xrltmin  10772  xrmaxle  10773  xrlemin  10774  ifle  10785  expmulnbnd  11513  limsupgre  12277  isumless  12627  cvgrat  12662  rpnnen2lem4  12819  ruclem2  12833  sadcaddlem  12971  sadadd3  12975  pcmptdvds  13265  prmreclem5  13290  prmreclem6  13291  pnfnei  17286  mnfnei  17287  xkopt  17689  xmetrtri2  18388  stdbdxmet  18547  stdbdmet  18548  stdbdmopn  18550  xrsxmet  18842  icccmplem2  18856  metdscn  18888  metnrmlem1a  18890  ivthlem2  19351  ovolicc2lem5  19419  ioombl1lem1  19454  ioombl1lem4  19457  ismbfd  19534  mbfi1fseqlem4  19612  mbfi1fseqlem5  19613  itg2const  19634  itg2const2  19635  itg2monolem3  19646  itg2gt0  19654  itg2cnlem1  19655  itg2cnlem2  19656  iblss  19698  itgless  19710  ibladdlem  19713  iblabsr  19723  iblmulc2  19724  dvferm1lem  19870  dvferm2lem  19872  dvlip2  19881  dgradd2  20188  plydiveu  20217  chtppilim  21171  dchrvmasumiflem1  21197  ostth3  21334  mblfinlem2  26246  itg2addnclem  26258  itg2addnc  26261  itg2gt0cn  26262  ibladdnclem  26263  iblmulc2nc  26272  bddiblnc  26277  ftc1anclem5  26286  ftc1anclem8  26289  ftc1anc  26290
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-if 3742
  Copyright terms: Public domain W3C validator