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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-if 4529

This theorem is referenced by:  ifcl  4573  keephyp  4599  soltmin  6135  xrmaxlt  13157  xrltmin  13158  xrmaxle  13159  xrlemin  13160  ifle  13173  expmulnbnd  14195  limsupgre  15422  isumless  15788  cvgrat  15826  rpnnen2lem4  16157  ruclem2  16172  sadcaddlem  16395  sadadd3  16399  pcmptdvds  16824  prmreclem5  16850  prmreclem6  16851  pnfnei  22716  mnfnei  22717  xkopt  23151  xmetrtri2  23854  stdbdxmet  24016  stdbdmet  24017  stdbdmopn  24019  xrsxmet  24317  icccmplem2  24331  metdscn  24364  metnrmlem1a  24366  ivthlem2  24961  ovolicc2lem5  25030  ioombl1lem1  25067  ioombl1lem4  25070  ismbfd  25148  mbfi1fseqlem4  25228  mbfi1fseqlem5  25229  itg2const  25250  itg2const2  25251  itg2monolem3  25262  itg2gt0  25270  itg2cnlem1  25271  itg2cnlem2  25272  iblss  25314  itgless  25326  ibladdlem  25329  iblabsr  25339  iblmulc2  25340  bddiblnc  25351  dvferm1lem  25493  dvferm2lem  25495  dvlip2  25504  dgradd2  25774  plydiveu  25803  chtppilim  26968  dchrvmasumiflem1  26994  ostth3  27131  1smat1  32773  poimirlem24  36501  mblfinlem2  36515  itg2addnclem  36528  itg2addnc  36531  itg2gt0cn  36532  ibladdnclem  36533  iblmulc2nc  36542  ftc1anclem5  36554  ftc1anclem8  36557  ftc1anc  36558