Theorem syl3an1 1181

Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.)

Hypotheses

Ref	Expression
syl3an1.1	⊢ (𝜑 → 𝜓)
syl3an1.2	⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)

Assertion

Ref	Expression
syl3an1	⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)

Proof of Theorem syl3an1

Step	Hyp	Ref	Expression
1		syl3an1.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	3anim1i 1170	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → (𝜓 ∧ 𝜒 ∧ 𝜃))
3		syl3an1.2	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)
4	2, 3	syl 18	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

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  df-3an 1105

This theorem is used by:  3adant1l  1195  3adant1r  1196  syl3an1b  1430  syl3an1br  1433  wefrc  5649  tz7.5  6378  f1resrcmplf1dlem  7271  f1cdmsn  7283  f1ofvswap  7307  f1ofveu  7407  fovcdmda  7585  suppvalfng  8165  smoiso  8351  odi  8566  nndi  8611  nnmsucr  8613  f1oen2g  8974  f1dom2g  8975  domssex2  9135  dif1ennn  9157  enfii  9180  phplem2  9199  php  9201  php3  9203  findcard3  9253  ordunifi  9260  nnsdomg  9269  ackbij1lem16  10236  divneg  11930  divdiv32  11947  divneg2  11963  ltdiv2  12125  fimaxre  12183  fiminre  12186  suprzcl  12701  peano2uz  12950  infssuzle  12980  lbzbi  12985  zbtwnre  12995  irrmul  13024  supxrunb1  13371  expnlbnd  14297  hash1to3  14557  fun2dmnop  14570  brfi1uzind  14573  brcnvtrclfvcnv  15078  retancl  16230  tanneg  16236  demoivreALT  16289  dvdscmulr  16374  dvdsmulcr  16375  mulmoddvds  16420  gcd0id  16609  euclemma  16804  phiprmpw  16867  fermltl  16875  vdwapun  17066  vdwapid1  17067  cshwshashlem1  17187  fsets  17261  pospo  18431  tltnle  18508  latasymb  18530  mgmn0plusgf  18741  sgrpcl  18828  mndcl  18844  imasmnd2  18881  gsumsgrpccat  18949  grpcl  19065  dfgrp2  19086  grprcan  19097  grpsubcl  19143  imasgrp2  19178  mhmid  19186  mhmmnd  19187  mulginvcom  19222  mulgnndir  19226  mulgnnass  19232  qusgrp  19314  ghmmulg  19355  ghmrn  19356  ghmeqker  19370  gsumccatsymgsn  19553  ablcom  19926  ablinvadd  19934  mulgmhm  19954  mulgghm  19955  ghmcmn  19958  odadd1  19975  odadd2  19976  rngacl  20297  rngcl  20299  rngpropd  20309  srgcl  20332  srgacl  20344  srgcom  20345  ringcl  20389  crngcom  20390  ringacl  20419  pwspjmhmmgpd  20468  imasring  20471  irredlmul  20569  rhmadd  20629  rhmsub  20630  rhmmul  20631  subrngacl  20718  subrgacl  20745  subrgmcl  20746  subrgugrp  20753  isdomn4  20877  isdrngd  20931  isdrngdOLD  20933  ringen1zr0  20944  srngadd  21017  srngmul  21018  idsrngd  21022  lmodacl  21056  lmodmcl  21057  lmodvacl  21059  lmodvsubcl  21091  lmod4  21096  lmodvaddsub4  21098  lmodvpncan  21099  lmodvnpcan  21100  lmodsubeq0  21105  pwssplit3  21245  islbs2  21341  islbs3  21342  lbsext  21350  rspssp  21431  cringm4  21534  nzerooringczr  21693  zlmlmod  21735  psgnco  21796  ipdir  21852  ip2eq  21866  ocvin  21887  frlmsplit2  21986  ascldimul  22103  rnasclmulcl  22109  mplbas2  22258  coe1add  22490  coe1subfv  22492  coe1mul2  22495  rhmply1vsca  22610  ringvcl  22622  matunitlindflem1  22901  cramer  22916  chpmat1d  23061  filin  24080  filfinnfr  24103  filuni  24111  ufprim  24135  uffinfix  24153  hausflf  24223  uffcfflf  24265  cnextcn  24293  tmdmulg  24318  tsmsxplem1  24379  psmetcl  24533  xmetcl  24557  metcl  24558  meteq0  24565  metge0  24571  metsym  24576  metgt0  24585  blelrnps  24642  blelrn  24643  blssm  24644  blres  24657  mscl  24687  xmscl  24688  xmsge0  24689  xmseq0  24690  xmssym  24691  mopnin  24723  nmf2  24819  ngpdsr  24831  ngpds2  24832  ngpds2r  24833  ngpds3  24834  ngpds3r  24835  nmge0  24843  nmeq0  24844  nm2dif  24851  nmmul  24890  nlmmul0or  24909  nmods  24970  clmsub  25308  clmacl  25312  clmmcl  25313  clmsubcl  25314  clmvscl  25316  clmvsubval  25337  ncvsprp  25380  ncvsdif  25383  ncvspds  25389  cphnmvs  25418  cphipcl  25419  cphipcj  25427  cphorthcom  25429  cphipval2  25469  4cphipval2  25470  cphipval  25471  fmcfil  25500  mbfi1fseqlem3  25945  mbfi1fseqlem4  25946  mbfi1fseqlem5  25947  deg1ldgdomn  26319  drnguc1p  26399  quotval  26522  sincosq1sgn  26736  sincosq2sgn  26737  sincosq3sgn  26738  sincosq4sgn  26739  efabl  26787  lgsneg1  27558  dchrisumlem3  27727  bdayn0p1  28634  ax5seglem2  29386  usgredg2vtx  29679  uspgredg2vtxeu  29680  usgredg2vtxeu  29681  cplgr3v  29895  vtxdumgr0nedg  29953  swrdwlk  30147  clwlkclwwlk  30472  frgrncvvdeqlem8  30786  grpocl  30981  grpodivcl  31020  ablomuldiv  31033  ablodivdiv4  31035  ablonnncan1  31038  vccl  31044  nvgcl  31101  nvcom  31102  nvadd4  31106  nvscl  31107  nvmval  31123  nvmcl  31127  nmcvcn  31176  nmlnoubi  31277  isblo3i  31282  blometi  31284  dipsubdir  31329  hlpar2  31377  hlpar  31378  hlcom  31381  hlipcj  31392  hlipgt0  31395  his52  31568  shintcli  31810  chlub  31990  homulass  32283  adjadj  32417  nmophmi  32512  kbass6  32602  atcvatlem  32866  mdsymlem3  32886  mdsymlem5  32888  suppiniseg  33158  rexdiv  33371  tlt3  33410  toslublem  33412  tosglblem  33414  archiabllem1b  33632  archiabllem2  33637  slmdacl  33649  slmdmcl  33650  slmdvacl  33652  lidlincl  33858  evls1fldgencl  34180  aean  34755  fiunelcarsg  34827  probcun  34929  probdif  34931  cndprobin  34945  rankfilimbi  35609  cusgredgex  35720  satefvfmla1  36004  climuzcnv  36250  pibt2  38171  mblfinlem1  38406  mblfinlem2  38407  ftc1anclem6  38447  ssbnd  38538  heibor1  38560  exidcl  38626  rngocl  38651  rngogcl  38662  rngocom  38663  rngoa4  38666  rngosub  38680  rngonegmn1l  38691  rngonegmn1r  38692  ispridlc  38820  lshpcmp  39861  opltcon3b  40077  oldmm1  40090  olj01  40098  latm32  40104  omllaw4  40119  omllaw5N  40120  cmtcomlemN  40121  cmt2N  40123  cmtbr2N  40126  cmtbr3N  40127  cmtbr4N  40128  glbconxN  40251  hlexch1  40255  hlexch2  40256  hlexchb1  40257  hlexchb2  40258  hlexch3  40264  hlexch4N  40265  hlatexchb1  40266  hlatexchb2  40267  hlatexch1  40268  hlatexch2  40269  hlatle  40271  hlateq  40272  hlrelat1  40273  hlrelat2  40276  cvr1  40283  cvrval5  40288  cvrp  40289  atcvr1  40290  atcvr2  40291  cvrexchlem  40292  cvrexch  40293  dalem54  40599  pmaple  40634  pmap11  40635  paddass  40711  pmapj2N  40802  pmapocjN  40803  trlval2  41036  nnproddivdvdsd  42866  fsuppssind  43439  mhphf  43443  0prjspnlem  43469  grumnudlem  45109  eelT00  45527  eelTTT  45528  eelT11  45529  eelT12  45531  eelTT1  45532  eelT01  45533  mullimc  46446  mullimcf  46453  dvmptfprod  46773  stoweidlem52  46880  stoweidlem60  46888  focofob  47968  f1ocof1ob  47969  clnbgrgrim  48850  ply1mulgsum  49320  itschlc0xyqsol1  49696  sinhpcosh  50666  reseccl  50679  recsccl  50680  recotcl  50681  onetansqsecsq  50687