Theorem ifboth 4507

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542  ifcif 4467

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-if 4468

This theorem is referenced by:  ifcl  4513  keephyp  4539  soltmin  6091  xrmaxlt  13097  xrltmin  13098  xrmaxle  13099  xrlemin  13100  ifle  13113  expmulnbnd  14159  limsupgre  15405  isumless  15769  cvgrat  15807  rpnnen2lem4  16143  ruclem2  16158  sadcaddlem  16385  sadadd3  16389  pcmptdvds  16823  prmreclem5  16849  prmreclem6  16850  pnfnei  23163  mnfnei  23164  xkopt  23598  xmetrtri2  24299  stdbdxmet  24458  stdbdmet  24459  stdbdmopn  24461  xrsxmet  24753  icccmplem2  24767  metdscn  24800  metnrmlem1a  24802  ivthlem2  25397  ovolicc2lem5  25466  ioombl1lem1  25503  ioombl1lem4  25506  ismbfd  25584  mbfi1fseqlem4  25663  mbfi1fseqlem5  25664  itg2const  25685  itg2const2  25686  itg2monolem3  25697  itg2gt0  25705  itg2cnlem1  25706  itg2cnlem2  25707  iblss  25750  itgless  25762  ibladdlem  25765  iblabsr  25775  iblmulc2  25776  bddiblnc  25787  dvferm1lem  25929  dvferm2lem  25931  dvlip2  25941  dgradd2  26214  plydiveu  26246  chtppilim  27426  dchrvmasumiflem1  27452  ostth3  27589  1smat1  33954  poimirlem24  37956  mblfinlem2  37970  itg2addnclem  37983  itg2addnc  37986  itg2gt0cn  37987  ibladdnclem  37988  iblmulc2nc  37997  ftc1anclem5  38009  ftc1anclem8  38012  ftc1anc  38013