Theorem ifboth 4507

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

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

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 4468

This theorem is referenced by:  ifcl  4513  keephyp  4539  soltmin  6100  xrmaxlt  13133  xrltmin  13134  xrmaxle  13135  xrlemin  13136  ifle  13149  expmulnbnd  14197  limsupgre  15443  isumless  15810  cvgrat  15848  rpnnen2lem4  16184  ruclem2  16199  sadcaddlem  16426  sadadd3  16430  pcmptdvds  16865  prmreclem5  16891  prmreclem6  16892  pnfnei  23185  mnfnei  23186  xkopt  23620  xmetrtri2  24321  stdbdxmet  24480  stdbdmet  24481  stdbdmopn  24483  xrsxmet  24775  icccmplem2  24789  metdscn  24822  metnrmlem1a  24824  ivthlem2  25419  ovolicc2lem5  25488  ioombl1lem1  25525  ioombl1lem4  25528  ismbfd  25606  mbfi1fseqlem4  25685  mbfi1fseqlem5  25686  itg2const  25707  itg2const2  25708  itg2monolem3  25719  itg2gt0  25727  itg2cnlem1  25728  itg2cnlem2  25729  iblss  25772  itgless  25784  ibladdlem  25787  iblabsr  25797  iblmulc2  25798  bddiblnc  25809  dvferm1lem  25951  dvferm2lem  25953  dvlip2  25962  dgradd2  26233  plydiveu  26264  chtppilim  27438  dchrvmasumiflem1  27464  ostth3  27601  1smat1  33948  poimirlem24  37965  mblfinlem2  37979  itg2addnclem  37992  itg2addnc  37995  itg2gt0cn  37996  ibladdnclem  37997  iblmulc2nc  38006  ftc1anclem5  38018  ftc1anclem8  38021  ftc1anc  38022