Theorem ifboth 4563

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1534  ifcif 4524

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-if 4525

This theorem is referenced by:  ifcl  4569  keephyp  4595  soltmin  6136  xrmaxlt  13184  xrltmin  13185  xrmaxle  13186  xrlemin  13187  ifle  13200  expmulnbnd  14221  limsupgre  15449  isumless  15815  cvgrat  15853  rpnnen2lem4  16185  ruclem2  16200  sadcaddlem  16423  sadadd3  16427  pcmptdvds  16854  prmreclem5  16880  prmreclem6  16881  pnfnei  23111  mnfnei  23112  xkopt  23546  xmetrtri2  24249  stdbdxmet  24411  stdbdmet  24412  stdbdmopn  24414  xrsxmet  24712  icccmplem2  24726  metdscn  24759  metnrmlem1a  24761  ivthlem2  25368  ovolicc2lem5  25437  ioombl1lem1  25474  ioombl1lem4  25477  ismbfd  25555  mbfi1fseqlem4  25635  mbfi1fseqlem5  25636  itg2const  25657  itg2const2  25658  itg2monolem3  25669  itg2gt0  25677  itg2cnlem1  25678  itg2cnlem2  25679  iblss  25721  itgless  25733  ibladdlem  25736  iblabsr  25746  iblmulc2  25747  bddiblnc  25758  dvferm1lem  25903  dvferm2lem  25905  dvlip2  25915  dgradd2  26190  plydiveu  26220  chtppilim  27395  dchrvmasumiflem1  27421  ostth3  27558  1smat1  33341  poimirlem24  37052  mblfinlem2  37066  itg2addnclem  37079  itg2addnc  37082  itg2gt0cn  37083  ibladdnclem  37084  iblmulc2nc  37093  ftc1anclem5  37105  ftc1anclem8  37108  ftc1anc  37109