Theorem ifboth 4516

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

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

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 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-if 4477

This theorem is referenced by:  ifcl  4522  keephyp  4548  soltmin  6090  xrmaxlt  13090  xrltmin  13091  xrmaxle  13092  xrlemin  13093  ifle  13106  expmulnbnd  14152  limsupgre  15398  isumless  15762  cvgrat  15800  rpnnen2lem4  16136  ruclem2  16151  sadcaddlem  16378  sadadd3  16382  pcmptdvds  16816  prmreclem5  16842  prmreclem6  16843  pnfnei  23145  mnfnei  23146  xkopt  23580  xmetrtri2  24281  stdbdxmet  24440  stdbdmet  24441  stdbdmopn  24443  xrsxmet  24735  icccmplem2  24749  metdscn  24782  metnrmlem1a  24784  ivthlem2  25390  ovolicc2lem5  25459  ioombl1lem1  25496  ioombl1lem4  25499  ismbfd  25577  mbfi1fseqlem4  25656  mbfi1fseqlem5  25657  itg2const  25678  itg2const2  25679  itg2monolem3  25690  itg2gt0  25698  itg2cnlem1  25699  itg2cnlem2  25700  iblss  25743  itgless  25755  ibladdlem  25758  iblabsr  25768  iblmulc2  25769  bddiblnc  25780  dvferm1lem  25925  dvferm2lem  25927  dvlip2  25937  dgradd2  26211  plydiveu  26243  chtppilim  27423  dchrvmasumiflem1  27449  ostth3  27586  1smat1  33828  poimirlem24  37694  mblfinlem2  37708  itg2addnclem  37721  itg2addnc  37724  itg2gt0cn  37725  ibladdnclem  37726  iblmulc2nc  37735  ftc1anclem5  37747  ftc1anclem8  37750  ftc1anc  37751