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

Theorem ifboth 3815
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 748 . 2  |-  ( ( ( ps  /\  ch )  /\  ph )  ->  ps )
4 simplr 749 . 2  |-  ( ( ( ps  /\  ch )  /\  -.  ph )  ->  ch )
51, 2, 3, 4ifbothda 3814 1  |-  ( ( ps  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1364   ifcif 3781
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2416
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1702  df-clab 2422  df-cleq 2428  df-clel 2431  df-if 3782
This theorem is referenced by:  ifcl  3821  keephyp  3844  soltmin  5227  xrmaxlt  11143  xrltmin  11144  xrmaxle  11145  xrlemin  11146  ifle  11157  expmulnbnd  11982  limsupgre  12945  isumless  13293  cvgrat  13328  rpnnen2lem4  13485  ruclem2  13499  sadcaddlem  13638  sadadd3  13642  pcmptdvds  13941  prmreclem5  13966  prmreclem6  13967  pnfnei  18668  mnfnei  18669  xkopt  19072  xmetrtri2  19775  stdbdxmet  19934  stdbdmet  19935  stdbdmopn  19937  xrsxmet  20230  icccmplem2  20244  metdscn  20276  metnrmlem1a  20278  ivthlem2  20780  ovolicc2lem5  20848  ioombl1lem1  20883  ioombl1lem4  20886  ismbfd  20962  mbfi1fseqlem4  21040  mbfi1fseqlem5  21041  itg2const  21062  itg2const2  21063  itg2monolem3  21074  itg2gt0  21082  itg2cnlem1  21083  itg2cnlem2  21084  iblss  21126  itgless  21138  ibladdlem  21141  iblabsr  21151  iblmulc2  21152  dvferm1lem  21300  dvferm2lem  21302  dvlip2  21311  dgradd2  21622  plydiveu  21651  chtppilim  22611  dchrvmasumiflem1  22637  ostth3  22774  mblfinlem2  28275  itg2addnclem  28289  itg2addnc  28292  itg2gt0cn  28293  ibladdnclem  28294  iblmulc2nc  28303  bddiblnc  28308  ftc1anclem5  28317  ftc1anclem8  28320  ftc1anc  28321
  Copyright terms: Public domain W3C validator