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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1568  ifcif 4486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-if 4487

This theorem is referenced by:  ifcl  4532  keephyp  4558  soltmin  6136  xrmaxlt  13206  xrltmin  13207  xrmaxle  13208  xrlemin  13209  ifle  13222  expmulnbnd  14271  limsupgre  15532  isumless  15899  cvgrat  15937  rpnnen2lem4  16272  ruclem2  16287  sadcaddlem  16514  sadadd3  16518  pcmptdvds  16953  prmreclem5  16979  prmreclem6  16980  pnfnei  23356  mnfnei  23357  xkopt  23791  xmetrtri2  24492  stdbdxmet  24651  stdbdmet  24652  stdbdmopn  24654  xrsxmet  24946  icccmplem2  24960  metdscn  24993  metnrmlem1a  24995  ivthlem2  25590  ovolicc2lem5  25659  ioombl1lem1  25696  ioombl1lem4  25699  ismbfd  25777  mbfi1fseqlem4  25856  mbfi1fseqlem5  25857  itg2const  25878  itg2const2  25879  itg2monolem3  25890  itg2gt0  25898  itg2cnlem1  25899  itg2cnlem2  25900  iblss  25943  itgless  25955  ibladdlem  25958  iblabsr  25968  iblmulc2  25969  bddiblnc  25980  dvferm1lem  26122  dvferm2lem  26124  dvlip2  26133  dgradd2  26404  plydiveu  26438  chtppilim  27615  dchrvmasumiflem1  27641  ostth3  27778  1smat1  34160  poimirlem24  38261  mblfinlem2  38275  itg2addnclem  38288  itg2addnc  38291  itg2gt0cn  38292  ibladdnclem  38293  iblmulc2nc  38302  ftc1anclem5  38314  ftc1anclem8  38317  ftc1anc  38318