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

Theorem ifboth 3936
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 753 . 2  |-  ( ( ( ps  /\  ch )  /\  ph )  ->  ps )
4 simplr 754 . 2  |-  ( ( ( ps  /\  ch )  /\  -.  ph )  ->  ch )
51, 2, 3, 4ifbothda 3935 1  |-  ( ( ps  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1370   ifcif 3902
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-if 3903
This theorem is referenced by:  ifcl  3942  keephyp  3965  soltmin  5348  xrmaxlt  11268  xrltmin  11269  xrmaxle  11270  xrlemin  11271  ifle  11282  expmulnbnd  12117  limsupgre  13081  isumless  13430  cvgrat  13465  rpnnen2lem4  13622  ruclem2  13636  sadcaddlem  13775  sadadd3  13779  pcmptdvds  14078  prmreclem5  14103  prmreclem6  14104  pnfnei  18966  mnfnei  18967  xkopt  19370  xmetrtri2  20073  stdbdxmet  20232  stdbdmet  20233  stdbdmopn  20235  xrsxmet  20528  icccmplem2  20542  metdscn  20574  metnrmlem1a  20576  ivthlem2  21078  ovolicc2lem5  21146  ioombl1lem1  21182  ioombl1lem4  21185  ismbfd  21261  mbfi1fseqlem4  21339  mbfi1fseqlem5  21340  itg2const  21361  itg2const2  21362  itg2monolem3  21373  itg2gt0  21381  itg2cnlem1  21382  itg2cnlem2  21383  iblss  21425  itgless  21437  ibladdlem  21440  iblabsr  21450  iblmulc2  21451  dvferm1lem  21599  dvferm2lem  21601  dvlip2  21610  dgradd2  21878  plydiveu  21907  chtppilim  22867  dchrvmasumiflem1  22893  ostth3  23030  mblfinlem2  28600  itg2addnclem  28614  itg2addnc  28617  itg2gt0cn  28618  ibladdnclem  28619  iblmulc2nc  28628  bddiblnc  28633  ftc1anclem5  28642  ftc1anclem8  28645  ftc1anc  28646
  Copyright terms: Public domain W3C validator