Theorem ifboth 4525

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570  ifcif 4485

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-if 4486

This theorem is used by:  ifcl  4531  keephyp  4557  soltmin  6134  xrmaxlt  13235  xrltmin  13236  xrmaxle  13237  xrlemin  13238  ifle  13251  expmulnbnd  14301  limsupgre  15570  isumless  15936  cvgrat  15974  rpnnen2lem4  16309  ruclem2  16324  sadcaddlem  16551  sadadd3  16555  pcmptdvds  16990  prmreclem5  17016  prmreclem6  17017  pnfnei  23449  mnfnei  23450  xkopt  23885  xmetrtri2  24586  stdbdxmet  24745  stdbdmet  24746  stdbdmopn  24748  xrsxmet  25040  icccmplem2  25054  metdscn  25087  metnrmlem1a  25089  ivthlem2  25684  ovolicc2lem5  25753  ioombl1lem1  25790  ioombl1lem4  25793  ismbfd  25871  mbfi1fseqlem4  25950  mbfi1fseqlem5  25951  itg2const  25972  itg2const2  25973  itg2monolem3  25984  itg2gt0  25992  itg2cnlem1  25993  itg2cnlem2  25994  iblss  26037  itgless  26049  ibladdlem  26052  iblabsr  26062  iblmulc2  26063  bddiblnc  26074  dvferm1lem  26216  dvferm2lem  26218  dvlip2  26227  dgradd2  26498  plydiveu  26532  chtppilim  27712  dchrvmasumiflem1  27738  ostth3  27875  1smat1  34316  poimirlem24  38395  mblfinlem2  38409  itg2addnclem  38422  itg2addnc  38425  itg2gt0cn  38426  ibladdnclem  38427  iblmulc2nc  38436  ftc1anclem5  38448  ftc1anclem8  38451  ftc1anc  38452