Theorem ifboth 4567

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-if 4529

This theorem is referenced by:  ifcl  4573  keephyp  4599  soltmin  6137  xrmaxlt  13167  xrltmin  13168  xrmaxle  13169  xrlemin  13170  ifle  13183  expmulnbnd  14205  limsupgre  15432  isumless  15798  cvgrat  15836  rpnnen2lem4  16167  ruclem2  16182  sadcaddlem  16405  sadadd3  16409  pcmptdvds  16834  prmreclem5  16860  prmreclem6  16861  pnfnei  23044  mnfnei  23045  xkopt  23479  xmetrtri2  24182  stdbdxmet  24344  stdbdmet  24345  stdbdmopn  24347  xrsxmet  24645  icccmplem2  24659  metdscn  24692  metnrmlem1a  24694  ivthlem2  25301  ovolicc2lem5  25370  ioombl1lem1  25407  ioombl1lem4  25410  ismbfd  25488  mbfi1fseqlem4  25568  mbfi1fseqlem5  25569  itg2const  25590  itg2const2  25591  itg2monolem3  25602  itg2gt0  25610  itg2cnlem1  25611  itg2cnlem2  25612  iblss  25654  itgless  25666  ibladdlem  25669  iblabsr  25679  iblmulc2  25680  bddiblnc  25691  dvferm1lem  25836  dvferm2lem  25838  dvlip2  25848  dgradd2  26121  plydiveu  26150  chtppilim  27321  dchrvmasumiflem1  27347  ostth3  27484  1smat1  33248  poimirlem24  36976  mblfinlem2  36990  itg2addnclem  37003  itg2addnc  37006  itg2gt0cn  37007  ibladdnclem  37008  iblmulc2nc  37017  ftc1anclem5  37029  ftc1anclem8  37032  ftc1anc  37033