Theorem ifboth 4501

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547  ifcif 4461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-if 4462

This theorem is referenced by:  ifcl  4507  keephyp  4533  soltmin  6093  xrmaxlt  13131  xrltmin  13132  xrmaxle  13133  xrlemin  13134  ifle  13147  expmulnbnd  14195  limsupgre  15441  isumless  15808  cvgrat  15846  rpnnen2lem4  16182  ruclem2  16197  sadcaddlem  16424  sadadd3  16428  pcmptdvds  16863  prmreclem5  16889  prmreclem6  16890  pnfnei  23210  mnfnei  23211  xkopt  23645  xmetrtri2  24346  stdbdxmet  24505  stdbdmet  24506  stdbdmopn  24508  xrsxmet  24800  icccmplem2  24814  metdscn  24847  metnrmlem1a  24849  ivthlem2  25444  ovolicc2lem5  25513  ioombl1lem1  25550  ioombl1lem4  25553  ismbfd  25631  mbfi1fseqlem4  25710  mbfi1fseqlem5  25711  itg2const  25732  itg2const2  25733  itg2monolem3  25744  itg2gt0  25752  itg2cnlem1  25753  itg2cnlem2  25754  iblss  25797  itgless  25809  ibladdlem  25812  iblabsr  25822  iblmulc2  25823  bddiblnc  25834  dvferm1lem  25976  dvferm2lem  25978  dvlip2  25987  dgradd2  26258  plydiveu  26289  chtppilim  27463  dchrvmasumiflem1  27489  ostth3  27626  1smat1  33995  poimirlem24  38012  mblfinlem2  38026  itg2addnclem  38039  itg2addnc  38042  itg2gt0cn  38043  ibladdnclem  38044  iblmulc2nc  38053  ftc1anclem5  38065  ftc1anclem8  38068  ftc1anc  38069