Theorem ifboth 4518

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

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-if 4479

This theorem is referenced by:  ifcl  4524  keephyp  4550  soltmin  6089  xrmaxlt  13101  xrltmin  13102  xrmaxle  13103  xrlemin  13104  ifle  13117  expmulnbnd  14160  limsupgre  15406  isumless  15770  cvgrat  15808  rpnnen2lem4  16144  ruclem2  16159  sadcaddlem  16386  sadadd3  16390  pcmptdvds  16824  prmreclem5  16850  prmreclem6  16851  pnfnei  23123  mnfnei  23124  xkopt  23558  xmetrtri2  24260  stdbdxmet  24419  stdbdmet  24420  stdbdmopn  24422  xrsxmet  24714  icccmplem2  24728  metdscn  24761  metnrmlem1a  24763  ivthlem2  25369  ovolicc2lem5  25438  ioombl1lem1  25475  ioombl1lem4  25478  ismbfd  25556  mbfi1fseqlem4  25635  mbfi1fseqlem5  25636  itg2const  25657  itg2const2  25658  itg2monolem3  25669  itg2gt0  25677  itg2cnlem1  25678  itg2cnlem2  25679  iblss  25722  itgless  25734  ibladdlem  25737  iblabsr  25747  iblmulc2  25748  bddiblnc  25759  dvferm1lem  25904  dvferm2lem  25906  dvlip2  25916  dgradd2  26190  plydiveu  26222  chtppilim  27402  dchrvmasumiflem1  27428  ostth3  27565  1smat1  33770  poimirlem24  37623  mblfinlem2  37637  itg2addnclem  37650  itg2addnc  37653  itg2gt0cn  37654  ibladdnclem  37655  iblmulc2nc  37664  ftc1anclem5  37676  ftc1anclem8  37679  ftc1anc  37680