MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl3an3 Structured version   Visualization version   GIF version

Theorem syl3an3 1401
Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.)
Hypotheses
Ref Expression
syl3an3.1 (𝜑𝜃)
syl3an3.2 ((𝜓𝜒𝜃) → 𝜏)
Assertion
Ref Expression
syl3an3 ((𝜓𝜒𝜑) → 𝜏)

Proof of Theorem syl3an3
StepHypRef Expression
1 syl3an3.1 . . 3 (𝜑𝜃)
2 syl3an3.2 . . . 4 ((𝜓𝜒𝜃) → 𝜏)
323exp 1283 . . 3 (𝜓 → (𝜒 → (𝜃𝜏)))
41, 3syl7 74 . 2 (𝜓 → (𝜒 → (𝜑𝜏)))
543imp 1275 1 ((𝜓𝜒𝜑) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1054
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 197  df-an 385  df-3an 1056
This theorem is referenced by:  syl3an3b  1404  syl3an3br  1407  vtoclgftOLD  3286  disji  4669  ovmpt2x  6831  ovmpt2ga  6832  wfrlem14  7473  unbnn2  8258  axdc3lem4  9313  axdclem2  9380  gruiin  9670  gruen  9672  divass  10741  ltmul2  10912  xleadd1  12123  xltadd2  12125  xlemul1  12158  xltmul2  12161  elfzo  12511  modcyc2  12746  faclbnd5  13125  relexprel  13823  subcn2  14369  mulcn2  14370  ndvdsp1  15182  gcddiv  15315  lcmneg  15363  lubel  17169  gsumccatsn  17427  mulgaddcom  17611  oddvdsi  18013  odcong  18014  odeq  18015  efgsp1  18196  lspsnss  19038  lindsmm2  20216  mulmarep1el  20426  mdetunilem4  20469  iuncld  20897  neips  20965  opnneip  20971  comppfsc  21383  hmeof1o2  21614  ordthmeo  21653  ufinffr  21780  elfm3  21801  utop3cls  22102  blcntrps  22264  blcntr  22265  neibl  22353  blnei  22354  metss  22360  stdbdmetval  22366  prdsms  22383  blval2  22414  lmmbr  23102  lmmbr2  23103  iscau2  23121  bcthlem1  23167  bcthlem3  23169  bcthlem4  23170  dvn2bss  23738  dvfsumrlim  23839  dvfsumrlim2  23840  cxpexpz  24458  cxpsub  24473  relogbzexp  24559  upgr4cycl4dv4e  27163  konigsbergssiedgwpr  27227  hvaddsub12  28023  hvaddsubass  28026  hvsubdistr1  28034  hvsubcan  28059  hhssnv  28249  spanunsni  28566  homco1  28788  homulass  28789  hoadddir  28791  hosubdi  28795  hoaddsubass  28802  hosubsub4  28805  lnopmi  28987  adjlnop  29073  mdsymlem5  29394  disjif  29517  disjif2  29520  ind0  30208  sigaclfu  30310  bnj544  31090  bnj561  31099  bnj562  31100  bnj594  31108  clsint2  32449  ftc1anclem6  33620  isbnd2  33712  blbnd  33716  isdrngo2  33887  atnem0  34923  hlrelat5N  35005  ltrnel  35743  ltrnat  35744  ltrncnvat  35745  jm2.22  37879  jm2.23  37880  dvconstbi  38850  eelT11  39249  eelT12  39251  eelTT1  39252  eelT01  39253  eel0T1  39254  liminfvalxr  40333  rmfsupp  42480  mndpfsupp  42482  scmfsupp  42484  dignn0flhalflem2  42735
  Copyright terms: Public domain W3C validator