Theorem ifboth 4521

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569  ifcif 4481

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-if 4482

This theorem is used by:  ifcl  4527  keephyp  4553  soltmin  6129  xrmaxlt  13312  xrltmin  13313  xrmaxle  13314  xrlemin  13315  ifle  13328  expmulnbnd  14380  limsupgre  15649  isumless  16015  cvgrat  16053  rpnnen2lem4  16386  ruclem2  16401  sadcaddlem  16628  sadadd3  16632  pcmptdvds  17073  prmreclem5  17099  prmreclem6  17100  pnfnei  23539  mnfnei  23540  xkopt  23975  xmetrtri2  24676  stdbdxmet  24835  stdbdmet  24836  stdbdmopn  24838  xrsxmet  25130  icccmplem2  25144  metdscn  25177  metnrmlem1a  25179  ivthlem2  25774  ovolicc2lem5  25843  ioombl1lem1  25880  ioombl1lem4  25883  ismbfd  25961  mbfi1fseqlem4  26040  mbfi1fseqlem5  26041  itg2const  26062  itg2const2  26063  itg2monolem3  26074  itg2gt0  26082  itg2cnlem1  26083  itg2cnlem2  26084  iblss  26126  itgless  26138  ibladdlem  26141  iblabsr  26151  iblmulc2  26152  bddiblnc  26163  dvferm1lem  26305  dvferm2lem  26307  dvlip2  26316  dgradd2  26588  plydiveu  26620  chtppilim  27803  dchrvmasumiflem1  27829  ostth3  27966  1smat1  34479  poimirlem24  38638  mblfinlem2  38652  itg2addnclem  38665  itg2addnc  38668  itg2gt0cn  38669  ibladdnclem  38670  iblmulc2nc  38679  ftc1anclem5  38691  ftc1anclem8  38694  ftc1anc  38695