Theorem ifboth 4425

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1525  ifcif 4387

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-ext 2771

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-ex 1766  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-if 4388

This theorem is referenced by:  ifcl  4431  keephyp  4456  soltmin  5879  xrmaxlt  12428  xrltmin  12429  xrmaxle  12430  xrlemin  12431  ifle  12444  expmulnbnd  13450  limsupgre  14676  isumless  15037  cvgrat  15076  rpnnen2lem4  15407  ruclem2  15422  sadcaddlem  15643  sadadd3  15647  pcmptdvds  16063  prmreclem5  16089  prmreclem6  16090  pnfnei  21516  mnfnei  21517  xkopt  21951  xmetrtri2  22653  stdbdxmet  22812  stdbdmet  22813  stdbdmopn  22815  xrsxmet  23104  icccmplem2  23118  metdscn  23151  metnrmlem1a  23153  ivthlem2  23740  ovolicc2lem5  23809  ioombl1lem1  23846  ioombl1lem4  23849  ismbfd  23927  mbfi1fseqlem4  24006  mbfi1fseqlem5  24007  itg2const  24028  itg2const2  24029  itg2monolem3  24040  itg2gt0  24048  itg2cnlem1  24049  itg2cnlem2  24050  iblss  24092  itgless  24104  ibladdlem  24107  iblabsr  24117  iblmulc2  24118  dvferm1lem  24268  dvferm2lem  24270  dvlip2  24279  dgradd2  24545  plydiveu  24574  chtppilim  25737  dchrvmasumiflem1  25763  ostth3  25900  1smat1  30680  poimirlem24  34468  mblfinlem2  34482  itg2addnclem  34495  itg2addnc  34498  itg2gt0cn  34499  ibladdnclem  34500  iblmulc2nc  34509  bddiblnc  34514  ftc1anclem5  34523  ftc1anclem8  34526  ftc1anc  34527