Theorem syl2anb 495

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 488	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
5	1, 4	sylan2b 491	1 ⊢ ((𝜑 ∧ 𝜏) → 𝜃)

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 196  df-an 385

This theorem is referenced by:  sylancb  696  reupick3  3871  difprsnss  4270  pwssun  4944  trin2  5438  sspred  5605  fundif  5849  fnun  5911  fco  5971  f1co  6023  foco  6038  f1oun  6069  f1oco  6072  eqfnfv  6219  eqfunfv  6224  sorpsscmpl  6846  ordsucsssuc  6915  ordsucun  6917  soxp  7177  ressuppssdif  7203  wfrlem4  7305  issmo  7332  tfrlem5  7363  ener  7888  enerOLD  7889  domtr  7895  unen  7925  xpdom2  7940  mapen  8009  unxpdomlem3  8051  fiin  8211  suc11reg  8399  xpnum  8660  pm54.43  8709  r0weon  8718  fseqen  8733  kmlem9  8863  axpre-lttrn  9866  axpre-mulgt0  9868  wloglei  10439  mulnzcnopr  10552  zaddcl  11294  zmulcl  11303  qaddcl  11680  qmulcl  11682  rpaddcl  11730  rpmulcl  11731  rpdivcl  11732  xrltnsym  11846  xrlttri  11848  xmullem  11966  xmulcom  11968  xmulneg1  11971  xmulf  11974  ge0addcl  12155  ge0mulcl  12156  ge0xaddcl  12157  ge0xmulcl  12158  serge0  12717  expclzlem  12746  expge0  12758  expge1  12759  hashfacen  13095  wwlktovf1  13548  qredeu  15210  nn0gcdsq  15298  mul4sq  15496  fpwipodrs  16987  gimco  17533  gictr  17540  symgextf1  17664  efgrelexlemb  17986  xrs1mnd  19603  lmimco  20002  lmictra  20003  cctop  20620  iscn2  20852  iscnp2  20853  paste  20908  txuni  21205  txcn  21239  txcmpb  21257  tx2ndc  21264  hmphtr  21396  snfil  21478  supfil  21509  filssufilg  21525  tsmsxp  21768  dscmet  22187  rlimcnp  24492  efnnfsumcl  24629  efchtdvds  24685  lgsne0  24860  mul2sq  24944  colinearalglem2  25587  nb3graprlem2  25981  wlkntrllem3  26091  wlknwwlknsur  26240  wlkiswwlksur  26247  wwlkextinj  26258  frgra3v  26529  hsn0elch  27489  shscli  27560  hsupss  27584  5oalem6  27902  mdsldmd1i  28574  superpos  28597  bnj110  30182  msubco  30682  poseq  30994  frrlem4  31027  sltsolem1  31067  fnsingle  31196  funimage  31205  funpartfun  31220  bj-snsetex  32144  riscer  32957  divrngidl  32997  mzpincl  36315  kelac2lem  36652  rp-fakenanass  36879  cllem0  36890  unhe1  37099  tz6.12-1-afv  39903  prmdvdsfmtnof1lem2  40035  nb3grprlem2  40609  cplgr3v  40657  crctcsh1wlkn0  41024  wlknwwlksnsur  41087  wlkwwlksur  41094  wwlksnextinj  41105  2zrngamgm  41729  2zrngmmgm  41736