Theorem ifboth 4520

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-if 4481

This theorem is referenced by:  ifcl  4526  keephyp  4552  soltmin  6094  xrmaxlt  13100  xrltmin  13101  xrmaxle  13102  xrlemin  13103  ifle  13116  expmulnbnd  14162  limsupgre  15408  isumless  15772  cvgrat  15810  rpnnen2lem4  16146  ruclem2  16161  sadcaddlem  16388  sadadd3  16392  pcmptdvds  16826  prmreclem5  16852  prmreclem6  16853  pnfnei  23168  mnfnei  23169  xkopt  23603  xmetrtri2  24304  stdbdxmet  24463  stdbdmet  24464  stdbdmopn  24466  xrsxmet  24758  icccmplem2  24772  metdscn  24805  metnrmlem1a  24807  ivthlem2  25413  ovolicc2lem5  25482  ioombl1lem1  25519  ioombl1lem4  25522  ismbfd  25600  mbfi1fseqlem4  25679  mbfi1fseqlem5  25680  itg2const  25701  itg2const2  25702  itg2monolem3  25713  itg2gt0  25721  itg2cnlem1  25722  itg2cnlem2  25723  iblss  25766  itgless  25778  ibladdlem  25781  iblabsr  25791  iblmulc2  25792  bddiblnc  25803  dvferm1lem  25948  dvferm2lem  25950  dvlip2  25960  dgradd2  26234  plydiveu  26266  chtppilim  27446  dchrvmasumiflem1  27472  ostth3  27609  1smat1  33942  poimirlem24  37816  mblfinlem2  37830  itg2addnclem  37843  itg2addnc  37846  itg2gt0cn  37847  ibladdnclem  37848  iblmulc2nc  37857  ftc1anclem5  37869  ftc1anclem8  37872  ftc1anc  37873