Theorem ifboth 4525

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 4524	1 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-if 4486

This theorem is used by:  ifcl  4531  keephyp  4557  soltmin  6142  xrmaxlt  13338  xrltmin  13339  xrmaxle  13340  xrlemin  13341  ifle  13354  expmulnbnd  14406  limsupgre  15677  isumless  16043  cvgrat  16081  rpnnen2lem4  16414  ruclem2  16429  sadcaddlem  16656  sadadd3  16660  pcmptdvds  17101  prmreclem5  17127  prmreclem6  17128  pnfnei  23568  mnfnei  23569  xkopt  24004  xmetrtri2  24705  stdbdxmet  24864  stdbdmet  24865  stdbdmopn  24867  xrsxmet  25159  icccmplem2  25173  metdscn  25206  metnrmlem1a  25208  ivthlem2  25803  ovolicc2lem5  25872  ioombl1lem1  25909  ioombl1lem4  25912  ismbfd  25990  mbfi1fseqlem4  26069  mbfi1fseqlem5  26070  itg2const  26091  itg2const2  26092  itg2monolem3  26103  itg2gt0  26111  itg2cnlem1  26112  itg2cnlem2  26113  iblss  26155  itgless  26167  ibladdlem  26170  iblabsr  26180  iblmulc2  26181  bddiblnc  26192  dvferm1lem  26334  dvferm2lem  26336  dvlip2  26345  dgradd2  26617  plydiveu  26649  chtppilim  27832  dchrvmasumiflem1  27858  ostth3  27995  1smat1  34506  poimirlem24  38754  mblfinlem2  38768  itg2addnclem  38781  itg2addnc  38784  itg2gt0cn  38785  ibladdnclem  38786  iblmulc2nc  38795  ftc1anclem5  38807  ftc1anclem8  38810  ftc1anc  38811