Theorem ifboth 4513

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

Step	Hyp	Ref	Expression
1		ifboth.1	. 2 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜃))
2		ifboth.2	. 2 ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒 ↔ 𝜃))
3		simpll 766	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜑) → 𝜓)
4		simplr 768	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ ¬ 𝜑) → 𝜒)
5	1, 2, 3, 4	ifbothda 4512	1 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541  ifcif 4473

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-if 4474

This theorem is referenced by:  ifcl  4519  keephyp  4545  soltmin  6080  xrmaxlt  13072  xrltmin  13073  xrmaxle  13074  xrlemin  13075  ifle  13088  expmulnbnd  14134  limsupgre  15380  isumless  15744  cvgrat  15782  rpnnen2lem4  16118  ruclem2  16133  sadcaddlem  16360  sadadd3  16364  pcmptdvds  16798  prmreclem5  16824  prmreclem6  16825  pnfnei  23128  mnfnei  23129  xkopt  23563  xmetrtri2  24264  stdbdxmet  24423  stdbdmet  24424  stdbdmopn  24426  xrsxmet  24718  icccmplem2  24732  metdscn  24765  metnrmlem1a  24767  ivthlem2  25373  ovolicc2lem5  25442  ioombl1lem1  25479  ioombl1lem4  25482  ismbfd  25560  mbfi1fseqlem4  25639  mbfi1fseqlem5  25640  itg2const  25661  itg2const2  25662  itg2monolem3  25673  itg2gt0  25681  itg2cnlem1  25682  itg2cnlem2  25683  iblss  25726  itgless  25738  ibladdlem  25741  iblabsr  25751  iblmulc2  25752  bddiblnc  25763  dvferm1lem  25908  dvferm2lem  25910  dvlip2  25920  dgradd2  26194  plydiveu  26226  chtppilim  27406  dchrvmasumiflem1  27432  ostth3  27569  1smat1  33807  poimirlem24  37663  mblfinlem2  37677  itg2addnclem  37690  itg2addnc  37693  itg2gt0cn  37694  ibladdnclem  37695  iblmulc2nc  37704  ftc1anclem5  37716  ftc1anclem8  37719  ftc1anc  37720