Theorem syl2anb 291

Description: A double syllogism inference. (Contributed by NM, 29-Jul-1999.)

Hypotheses

Ref	Expression
syl2anb.1	⊢ (𝜑 ↔ 𝜓)
syl2anb.2	⊢ (𝜏 ↔ 𝜒)
syl2anb.3	⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
syl2anb	⊢ ((𝜑 ∧ 𝜏) → 𝜃)

Proof of Theorem syl2anb

Step	Hyp	Ref	Expression
1		syl2anb.2	. 2 ⊢ (𝜏 ↔ 𝜒)
2		syl2anb.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
3		syl2anb.3	. . 3 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	sylanb 284	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
5	1, 4	sylan2b 287	1 ⊢ ((𝜑 ∧ 𝜏) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylancb  418  stdcndc  849  reupick3  3469  difprsnss  3785  trin2  5096  fundif  5341  imadiflem  5376  fnun  5405  fco  5465  f1co  5519  foco  5535  f1oun  5568  f1oco  5571  eqfunfv  5710  ftpg  5796  issmo  6404  tfrlem5  6430  ener  6901  domtr  6907  unen  6939  xpdom2  6958  mapen  6975  pm54.43  7331  axpre-lttrn  8039  axpre-mulgt0  8042  zmulcl  9468  qaddcl  9798  qmulcl  9800  rpaddcl  9841  rpmulcl  9842  rpdivcl  9843  xrltnsym  9957  xrlttri3  9961  ge0addcl  10145  ge0mulcl  10146  ge0xaddcl  10147  expclzaplem  10752  expge0  10764  expge1  10765  hashfacen  11025  qredeu  12585  nn0gcdsq  12688  mul4sq  12883  cnovex  14835  iscn2  14839  txuni  14902  txcn  14914  lgsne0  15682  mul2sq  15760