Theorem syl2anb 610

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  sylancb  612  rexdifi  4097  reupick3  4276  difprsnss  4762  opthhausdorff  5490  pwssun  5543  trin2  6115  sspred  6306  fundif  6581  fnun  6645  f1cof1  6782  f1oun  6836  f1oco  6840  eqfnfv  7021  eqfunfv  7027  sorpsscmpl  7739  ordsucsssuc  7823  ordsucun  7825  resf1extb  7935  soxp  8130  poseq  8159  ressuppssdif  8186  frrlem4  8291  issmo  8340  tfrlem5  8371  ener  9012  domtr  9018  unen  9057  xpdom2  9075  mapen  9144  unxpdomlem3  9233  fiin  9398  suc11reg  9604  djuunxp  9983  xpnum  10013  pm54.43  10063  r0weon  10072  fseqen  10087  kmlem9  10218  axpre-lttrn  11232  axpre-mulgt0  11234  wloglei  11829  mulnzcnf  11943  zaddcl  12717  zmulcl  12726  qaddcl  13074  qmulcl  13076  rpaddcl  13125  rpmulcl  13126  rpdivcl  13128  xrltnsym  13247  xrlttri  13249  xmullem  13375  xmulcom  13377  xmulneg1  13380  xmulf  13383  ge0addcl  13572  ge0mulcl  13573  ge0xaddcl  13574  ge0xmulcl  13575  serge0  14179  expclzlem  14206  expge0  14221  expge1  14222  hashfacen  14579  wwlktovf1  15090  nn0rppwr  16715  nn0expgcd  16718  qredeu  16813  nn0gcdsq  16908  mul4sq  17112  fpwipodrs  18694  pwmnd  19123  gimco  19462  gictr  19470  symgextf1  19615  efgrelexlemb  19944  rimco  20727  rictr  20732  xrs1mnd  21726  pzriprnglem5  21771  pzriprnglem8  21774  lmimco  22130  lmictra  22131  cctop  23304  iscn2  23536  iscnp2  23537  paste  23592  txuni  23891  txcn  23925  txcmpb  23943  tx2ndc  23950  hmphtr  24082  snfil  24163  supfil  24194  filssufilg  24210  tsmsxp  24454  dscmet  24871  rlimcnp  27275  efnnfsumcl  27412  efchtdvds  27468  lgsne0  27644  mul2sq  27728  ltssolem1  28014  z12addscl  28845  colinearalglem2  29467  nb3grprlem2  29944  cplgr3v  29998  crctcshwlkn0  30392  wwlksnextinj  30470  hsn0elch  31832  shscli  31901  hsupss  31925  5oalem6  32243  mdsldmd1i  32915  superpos  32938  bnj110  35471  scottsn  35728  msubco  36265  fnsingle  36651  funimage  36660  funpartfun  36677  mpomulnzcnf  37058  bj-nnfan  37626  bj-nnfor  37628  bj-snsetex  37846  bj-axseprep  37958  bj-snmoore  38002  difunieq  38265  riscer  38890  divrngidl  38930  dvdsexpnn0  43354  zaddcom  43496  zmulcom  43500  mzpincl  43698  kelac2lem  44024  omcl3g  44294  cllem0  44525  unhe1  44744  permaxun  45953  tz6.12-1-afv  48188  tz6.12-1-afv2  48255  sprsymrelf1  48522  prmdvdsfmtnof1lem2  48614  grictr  48965  usgrexmpl2trifr  49079  gpgprismgr4cycllem7  49143  uspgrsprf1  49189  2zrngamgm  49286  2zrngmmgm  49293  rrx2xpref1o  49774  f1omoOLD  49946