Theorem ifboth 4498

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539  ifcif 4459

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-if 4460

This theorem is referenced by:  ifcl  4504  keephyp  4530  soltmin  6041  xrmaxlt  12915  xrltmin  12916  xrmaxle  12917  xrlemin  12918  ifle  12931  expmulnbnd  13950  limsupgre  15190  isumless  15557  cvgrat  15595  rpnnen2lem4  15926  ruclem2  15941  sadcaddlem  16164  sadadd3  16168  pcmptdvds  16595  prmreclem5  16621  prmreclem6  16622  pnfnei  22371  mnfnei  22372  xkopt  22806  xmetrtri2  23509  stdbdxmet  23671  stdbdmet  23672  stdbdmopn  23674  xrsxmet  23972  icccmplem2  23986  metdscn  24019  metnrmlem1a  24021  ivthlem2  24616  ovolicc2lem5  24685  ioombl1lem1  24722  ioombl1lem4  24725  ismbfd  24803  mbfi1fseqlem4  24883  mbfi1fseqlem5  24884  itg2const  24905  itg2const2  24906  itg2monolem3  24917  itg2gt0  24925  itg2cnlem1  24926  itg2cnlem2  24927  iblss  24969  itgless  24981  ibladdlem  24984  iblabsr  24994  iblmulc2  24995  bddiblnc  25006  dvferm1lem  25148  dvferm2lem  25150  dvlip2  25159  dgradd2  25429  plydiveu  25458  chtppilim  26623  dchrvmasumiflem1  26649  ostth3  26786  1smat1  31754  poimirlem24  35801  mblfinlem2  35815  itg2addnclem  35828  itg2addnc  35831  itg2gt0cn  35832  ibladdnclem  35833  iblmulc2nc  35842  ftc1anclem5  35854  ftc1anclem8  35857  ftc1anc  35858