Theorem ifboth 4531

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-if 4492

This theorem is referenced by:  ifcl  4537  keephyp  4563  soltmin  6112  xrmaxlt  13148  xrltmin  13149  xrmaxle  13150  xrlemin  13151  ifle  13164  expmulnbnd  14207  limsupgre  15454  isumless  15818  cvgrat  15856  rpnnen2lem4  16192  ruclem2  16207  sadcaddlem  16434  sadadd3  16438  pcmptdvds  16872  prmreclem5  16898  prmreclem6  16899  pnfnei  23114  mnfnei  23115  xkopt  23549  xmetrtri2  24251  stdbdxmet  24410  stdbdmet  24411  stdbdmopn  24413  xrsxmet  24705  icccmplem2  24719  metdscn  24752  metnrmlem1a  24754  ivthlem2  25360  ovolicc2lem5  25429  ioombl1lem1  25466  ioombl1lem4  25469  ismbfd  25547  mbfi1fseqlem4  25626  mbfi1fseqlem5  25627  itg2const  25648  itg2const2  25649  itg2monolem3  25660  itg2gt0  25668  itg2cnlem1  25669  itg2cnlem2  25670  iblss  25713  itgless  25725  ibladdlem  25728  iblabsr  25738  iblmulc2  25739  bddiblnc  25750  dvferm1lem  25895  dvferm2lem  25897  dvlip2  25907  dgradd2  26181  plydiveu  26213  chtppilim  27393  dchrvmasumiflem1  27419  ostth3  27556  1smat1  33801  poimirlem24  37645  mblfinlem2  37659  itg2addnclem  37672  itg2addnc  37675  itg2gt0cn  37676  ibladdnclem  37677  iblmulc2nc  37686  ftc1anclem5  37698  ftc1anclem8  37701  ftc1anc  37702