Theorem ifboth 4526

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1569  ifcif 4486

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-if 4487

This theorem is used by:  ifcl  4532  keephyp  4558  soltmin  6135  xrmaxlt  13213  xrltmin  13214  xrmaxle  13215  xrlemin  13216  ifle  13229  expmulnbnd  14278  limsupgre  15539  isumless  15906  cvgrat  15944  rpnnen2lem4  16279  ruclem2  16294  sadcaddlem  16521  sadadd3  16525  pcmptdvds  16960  prmreclem5  16986  prmreclem6  16987  pnfnei  23388  mnfnei  23389  xkopt  23823  xmetrtri2  24524  stdbdxmet  24683  stdbdmet  24684  stdbdmopn  24686  xrsxmet  24978  icccmplem2  24992  metdscn  25025  metnrmlem1a  25027  ivthlem2  25622  ovolicc2lem5  25691  ioombl1lem1  25728  ioombl1lem4  25731  ismbfd  25809  mbfi1fseqlem4  25888  mbfi1fseqlem5  25889  itg2const  25910  itg2const2  25911  itg2monolem3  25922  itg2gt0  25930  itg2cnlem1  25931  itg2cnlem2  25932  iblss  25975  itgless  25987  ibladdlem  25990  iblabsr  26000  iblmulc2  26001  bddiblnc  26012  dvferm1lem  26154  dvferm2lem  26156  dvlip2  26165  dgradd2  26436  plydiveu  26470  chtppilim  27650  dchrvmasumiflem1  27676  ostth3  27813  1smat1  34203  poimirlem24  38323  mblfinlem2  38337  itg2addnclem  38350  itg2addnc  38353  itg2gt0cn  38354  ibladdnclem  38355  iblmulc2nc  38364  ftc1anclem5  38376  ftc1anclem8  38379  ftc1anc  38380