Theorem ifboth 4523

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1563  ifcif 4483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-if 4484

This theorem is referenced by:  ifcl  4529  keephyp  4555  soltmin  6127  xrmaxlt  13198  xrltmin  13199  xrmaxle  13200  xrlemin  13201  ifle  13214  expmulnbnd  14262  limsupgre  15522  isumless  15889  cvgrat  15927  rpnnen2lem4  16263  ruclem2  16278  sadcaddlem  16505  sadadd3  16509  pcmptdvds  16944  prmreclem5  16970  prmreclem6  16971  pnfnei  23338  mnfnei  23339  xkopt  23773  xmetrtri2  24474  stdbdxmet  24633  stdbdmet  24634  stdbdmopn  24636  xrsxmet  24928  icccmplem2  24942  metdscn  24975  metnrmlem1a  24977  ivthlem2  25572  ovolicc2lem5  25641  ioombl1lem1  25678  ioombl1lem4  25681  ismbfd  25759  mbfi1fseqlem4  25838  mbfi1fseqlem5  25839  itg2const  25860  itg2const2  25861  itg2monolem3  25872  itg2gt0  25880  itg2cnlem1  25881  itg2cnlem2  25882  iblss  25925  itgless  25937  ibladdlem  25940  iblabsr  25950  iblmulc2  25951  bddiblnc  25962  dvferm1lem  26104  dvferm2lem  26106  dvlip2  26115  dgradd2  26386  plydiveu  26420  chtppilim  27597  dchrvmasumiflem1  27623  ostth3  27760  1smat1  34111  poimirlem24  38155  mblfinlem2  38169  itg2addnclem  38182  itg2addnc  38185  itg2gt0cn  38186  ibladdnclem  38187  iblmulc2nc  38196  ftc1anclem5  38208  ftc1anclem8  38211  ftc1anc  38212