Theorem ifboth 4568

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542  ifcif 4529

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-if 4530

This theorem is referenced by:  ifcl  4574  keephyp  4600  soltmin  6138  xrmaxlt  13160  xrltmin  13161  xrmaxle  13162  xrlemin  13163  ifle  13176  expmulnbnd  14198  limsupgre  15425  isumless  15791  cvgrat  15829  rpnnen2lem4  16160  ruclem2  16175  sadcaddlem  16398  sadadd3  16402  pcmptdvds  16827  prmreclem5  16853  prmreclem6  16854  pnfnei  22724  mnfnei  22725  xkopt  23159  xmetrtri2  23862  stdbdxmet  24024  stdbdmet  24025  stdbdmopn  24027  xrsxmet  24325  icccmplem2  24339  metdscn  24372  metnrmlem1a  24374  ivthlem2  24969  ovolicc2lem5  25038  ioombl1lem1  25075  ioombl1lem4  25078  ismbfd  25156  mbfi1fseqlem4  25236  mbfi1fseqlem5  25237  itg2const  25258  itg2const2  25259  itg2monolem3  25270  itg2gt0  25278  itg2cnlem1  25279  itg2cnlem2  25280  iblss  25322  itgless  25334  ibladdlem  25337  iblabsr  25347  iblmulc2  25348  bddiblnc  25359  dvferm1lem  25501  dvferm2lem  25503  dvlip2  25512  dgradd2  25782  plydiveu  25811  chtppilim  26978  dchrvmasumiflem1  27004  ostth3  27141  1smat1  32784  poimirlem24  36512  mblfinlem2  36526  itg2addnclem  36539  itg2addnc  36542  itg2gt0cn  36543  ibladdnclem  36544  iblmulc2nc  36553  ftc1anclem5  36565  ftc1anclem8  36568  ftc1anc  36569