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

Theorem ifboth 4526
Description: A wff 𝜃 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 (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓𝜃))
ifboth.2 (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒𝜃))
Assertion
Ref Expression
ifboth ((𝜓𝜒) → 𝜃)

Proof of Theorem ifboth
StepHypRef Expression
1 ifboth.1 . 2 (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓𝜃))
2 ifboth.2 . 2 (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒𝜃))
3 simpll 766 . 2 (((𝜓𝜒) ∧ 𝜑) → 𝜓)
4 simplr 768 . 2 (((𝜓𝜒) ∧ ¬ 𝜑) → 𝜒)
51, 2, 3, 4ifbothda 4525 1 ((𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397   = wceq 1542  ifcif 4487
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-if 4488
This theorem is referenced by:  ifcl  4532  keephyp  4558  soltmin  6091  xrmaxlt  13101  xrltmin  13102  xrmaxle  13103  xrlemin  13104  ifle  13117  expmulnbnd  14139  limsupgre  15364  isumless  15731  cvgrat  15769  rpnnen2lem4  16100  ruclem2  16115  sadcaddlem  16338  sadadd3  16342  pcmptdvds  16767  prmreclem5  16793  prmreclem6  16794  pnfnei  22574  mnfnei  22575  xkopt  23009  xmetrtri2  23712  stdbdxmet  23874  stdbdmet  23875  stdbdmopn  23877  xrsxmet  24175  icccmplem2  24189  metdscn  24222  metnrmlem1a  24224  ivthlem2  24819  ovolicc2lem5  24888  ioombl1lem1  24925  ioombl1lem4  24928  ismbfd  25006  mbfi1fseqlem4  25086  mbfi1fseqlem5  25087  itg2const  25108  itg2const2  25109  itg2monolem3  25120  itg2gt0  25128  itg2cnlem1  25129  itg2cnlem2  25130  iblss  25172  itgless  25184  ibladdlem  25187  iblabsr  25197  iblmulc2  25198  bddiblnc  25209  dvferm1lem  25351  dvferm2lem  25353  dvlip2  25362  dgradd2  25632  plydiveu  25661  chtppilim  26826  dchrvmasumiflem1  26852  ostth3  26989  1smat1  32388  poimirlem24  36105  mblfinlem2  36119  itg2addnclem  36132  itg2addnc  36135  itg2gt0cn  36136  ibladdnclem  36137  iblmulc2nc  36146  ftc1anclem5  36158  ftc1anclem8  36161  ftc1anc  36162
  Copyright terms: Public domain W3C validator