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  5644  tz7.5  6385  f1resrcmplf1dlem  7280  f1cdmsn  7292  f1ofvswap  7316  f1ofveu  7416  fovcdmda  7594  suppvalfng  8189  smoiso  8375  tz7.48lem  8455  odi  8592  nndi  8637  nnmsucr  8639  f1oen2g  9000  f1dom2g  9001  domssex2  9161  dif1ennn  9183  enfii  9206  phplem2  9225  php  9227  php3  9229  findcard3  9279  ordunifi  9286  nnsdomg  9296  rankfilimbi  9907  ackbij1lem16  10317  divneg  12013  divdiv32  12030  divneg2  12046  ltdiv2  12208  fimaxre  12266  fiminre  12269  suprzcl  12784  peano2uz  13033  infssuzle  13063  lbzbi  13068  zbtwnre  13078  irrmul  13107  supxrunb1  13454  expnlbnd  14382  hash1to3  14642  fun2dmnop  14655  brfi1uzind  14658  brcnvtrclfvcnv  15165  retancl  16317  tanneg  16323  demoivreALT  16376  dvdscmulr  16461  dvdsmulcr  16462  mulmoddvds  16507  gcd0id  16698  euclemma  16896  phiprmpw  16960  fermltl  16968  vdwapun  17159  vdwapid1  17160  cshwshashlem1  17280  fsets  17354  pospo  18524  tltnle  18601  latasymb  18623  mgmn0plusgf  18834  sgrpcl  18922  mndcl  18938  imasmnd2  18975  gsumsgrpccat  19043  grpcl  19159  dfgrp2  19180  grprcan  19191  grpsubcl  19237  imasgrp2  19272  mhmid  19280  mhmmnd  19281  mulginvcom  19316  mulgnndir  19320  mulgnnass  19326  qusgrp  19408  ghmmulg  19449  ghmrn  19450  ghmeqker  19464  gsumccatsymgsn  19647  ablcom  20020  ablinvadd  20028  mulgmhm  20048  mulgghm  20049  ghmcmn  20052  odadd1  20069  odadd2  20070  rngacl  20391  rngcl  20393  rngpropd  20403  srgcl  20426  srgacl  20438  srgcom  20439  ringcl  20484  crngcom  20485  ringacl  20514  pwspjmhmmgpd  20564  imasring  20567  irredlmul  20665  rhmadd  20725  rhmsub  20726  rhmmul  20727  subrngacl  20815  subrgacl  20842  subrgmcl  20843  subrgugrp  20850  isdomn4  20974  isdrngd  21029  isdrngdOLD  21031  ringen1zr0  21042  srngadd  21115  srngmul  21116  idsrngd  21120  lmodacl  21154  lmodmcl  21155  lmodvacl  21157  lmodvsubcl  21189  lmod4  21194  lmodvaddsub4  21196  lmodvpncan  21197  lmodvnpcan  21198  lmodsubeq0  21203  pwssplit3  21343  islbs2  21439  islbs3  21440  lbsext  21448  rspssp  21529  cringm4  21634  nzerooringczr  21793  zlmlmod  21835  psgnco  21896  ipdir  21952  ip2eq  21966  ocvin  21987  frlmsplit2  22086  ascldimul  22203  rnasclmulcl  22209  mplbas2  22358  coe1add  22590  coe1subfv  22592  coe1mul2  22595  rhmply1vsca  22710  ringvcl  22722  matunitlindflem1  23001  cramer  23016  chpmat1d  23161  filin  24180  filfinnfr  24203  filuni  24211  ufprim  24235  uffinfix  24253  hausflf  24323  uffcfflf  24365  cnextcn  24393  tmdmulg  24418  tsmsxplem1  24479  psmetcl  24633  xmetcl  24657  metcl  24658  meteq0  24665  metge0  24671  metsym  24676  metgt0  24685  blelrnps  24742  blelrn  24743  blssm  24744  blres  24757  mscl  24787  xmscl  24788  xmsge0  24789  xmseq0  24790  xmssym  24791  mopnin  24823  nmf2  24919  ngpdsr  24931  ngpds2  24932  ngpds2r  24933  ngpds3  24934  ngpds3r  24935  nmge0  24943  nmeq0  24944  nm2dif  24951  nmmul  24990  nlmmul0or  25009  nmods  25070  clmsub  25408  clmacl  25412  clmmcl  25413  clmsubcl  25414  clmvscl  25416  clmvsubval  25437  ncvsprp  25480  ncvsdif  25483  ncvspds  25489  cphnmvs  25518  cphipcl  25519  cphipcj  25527  cphorthcom  25529  cphipval2  25569  4cphipval2  25570  cphipval  25571  fmcfil  25600  mbfi1fseqlem3  26045  mbfi1fseqlem4  26046  mbfi1fseqlem5  26047  deg1ldgdomn  26419  drnguc1p  26499  quotval  26620  sincosq1sgn  26834  sincosq2sgn  26835  sincosq3sgn  26836  sincosq4sgn  26837  efabl  26885  lgsneg1  27656  dchrisumlem3  27825  bdayn0p1  28762  ax5seglem2  29514  usgredg2vtx  29807  uspgredg2vtxeu  29808  usgredg2vtxeu  29809  cplgr3v  30023  vtxdumgr0nedg  30081  swrdwlk  30275  clwlkclwwlk  30600  frgrncvvdeqlem8  30914  grpocl  31109  grpodivcl  31148  ablomuldiv  31161  ablodivdiv4  31163  ablonnncan1  31166  vccl  31172  nvgcl  31229  nvcom  31230  nvadd4  31234  nvscl  31235  nvmval  31251  nvmcl  31255  nmcvcn  31304  nmlnoubi  31405  isblo3i  31410  blometi  31412  dipsubdir  31457  hlpar2  31505  hlpar  31506  hlcom  31509  hlipcj  31520  hlipgt0  31523  his52  31696  shintcli  31938  chlub  32118  homulass  32411  adjadj  32545  nmophmi  32640  kbass6  32730  atcvatlem  32994  mdsymlem3  33014  mdsymlem5  33016  suppiniseg  33328  rexdiv  33540  tlt3  33579  toslublem  33581  tosglblem  33583  archiabllem1b  33801  archiabllem2  33806  slmdacl  33818  slmdmcl  33819  slmdvacl  33821  lidlincl  34028  evls1fldgencl  34350  aean  34925  fiunelcarsg  34996  probcun  35098  probdif  35100  cndprobin  35114  cusgredgex  35984  satefvfmla1  36278  climuzcnv  36524  pibt2  38447  mblfinlem1  38682  mblfinlem2  38683  ftc1anclem6  38723  ssbnd  38829  heibor1  38851  exidcl  38917  rngocl  38942  rngogcl  38953  rngocom  38954  rngoa4  38957  rngosub  38971  rngonegmn1l  38982  rngonegmn1r  38983  ispridlc  39111  lshpcmp  40152  opltcon3b  40368  oldmm1  40381  olj01  40389  latm32  40395  omllaw4  40410  omllaw5N  40411  cmtcomlemN  40412  cmt2N  40414  cmtbr2N  40417  cmtbr3N  40418  cmtbr4N  40419  glbconxN  40542  hlexch1  40546  hlexch2  40547  hlexchb1  40548  hlexchb2  40549  hlexch3  40555  hlexch4N  40556  hlatexchb1  40557  hlatexchb2  40558  hlatexch1  40559  hlatexch2  40560  hlatle  40562  hlateq  40563  hlrelat1  40564  hlrelat2  40567  cvr1  40574  cvrval5  40579  cvrp  40580  atcvr1  40581  atcvr2  40582  cvrexchlem  40583  cvrexch  40584  dalem54  40890  pmaple  40925  pmap11  40926  paddass  41002  pmapj2N  41093  pmapocjN  41094  trlval2  41327  nnproddivdvdsd  43157  fsuppssind  43728  mhphf  43732  0prjspnlem  43769  grumnudlem  45376  eelT00  45794  eelTTT  45795  eelT11  45796  eelT12  45798  eelTT1  45799  eelT01  45800  mullimc  46735  mullimcf  46742  dvmptfprod  47062  stoweidlem52  47169  stoweidlem60  47177  focofob  48257  f1ocof1ob  48258  clnbgrgrim  49139  ply1mulgsum  49609  itschlc0xyqsol1  49985  sinhpcosh  51015  reseccl  51028  recsccl  51029  recotcl  51030  onetansqsecsq  51036