Theorem ifboth 4505

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 765	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜑) → 𝜓)
4		simplr 767	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ ¬ 𝜑) → 𝜒)
5	1, 2, 3, 4	ifbothda 4504	1 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537  ifcif 4467

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1781  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-if 4468

This theorem is referenced by:  ifcl  4511  keephyp  4536  soltmin  5996  xrmaxlt  12575  xrltmin  12576  xrmaxle  12577  xrlemin  12578  ifle  12591  expmulnbnd  13597  limsupgre  14838  isumless  15200  cvgrat  15239  rpnnen2lem4  15570  ruclem2  15585  sadcaddlem  15806  sadadd3  15810  pcmptdvds  16230  prmreclem5  16256  prmreclem6  16257  pnfnei  21828  mnfnei  21829  xkopt  22263  xmetrtri2  22966  stdbdxmet  23125  stdbdmet  23126  stdbdmopn  23128  xrsxmet  23417  icccmplem2  23431  metdscn  23464  metnrmlem1a  23466  ivthlem2  24053  ovolicc2lem5  24122  ioombl1lem1  24159  ioombl1lem4  24162  ismbfd  24240  mbfi1fseqlem4  24319  mbfi1fseqlem5  24320  itg2const  24341  itg2const2  24342  itg2monolem3  24353  itg2gt0  24361  itg2cnlem1  24362  itg2cnlem2  24363  iblss  24405  itgless  24417  ibladdlem  24420  iblabsr  24430  iblmulc2  24431  dvferm1lem  24581  dvferm2lem  24583  dvlip2  24592  dgradd2  24858  plydiveu  24887  chtppilim  26051  dchrvmasumiflem1  26077  ostth3  26214  1smat1  31069  poimirlem24  34931  mblfinlem2  34945  itg2addnclem  34958  itg2addnc  34961  itg2gt0cn  34962  ibladdnclem  34963  iblmulc2nc  34972  bddiblnc  34977  ftc1anclem5  34986  ftc1anclem8  34989  ftc1anc  34990