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

Theorem mpisyl 21
Description: A syllogism combined with a modus ponens inference. (Contributed by Alan Sare, 25-Jul-2011.)
Hypotheses
Ref Expression
mpisyl.1 (𝜑𝜓)
mpisyl.2 𝜒
mpisyl.3 (𝜓 → (𝜒𝜃))
Assertion
Ref Expression
mpisyl (𝜑𝜃)

Proof of Theorem mpisyl
StepHypRef Expression
1 mpisyl.1 . 2 (𝜑𝜓)
2 mpisyl.2 . . 3 𝜒
3 mpisyl.3 . . 3 (𝜓 → (𝜒𝜃))
42, 3mpi 20 . 2 (𝜓𝜃)
51, 4syl 17 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  ceqsex  3232  moeq3  3370  reusv1OLD  4832  fveqf1o  6512  fliftcnv  6516  fliftfun  6517  cnvct  7978  undom  7993  pwdom  8057  onomeneq  8095  pwfilem  8205  ordiso  8366  ordtypelem8  8375  wdompwdom  8428  unxpwdom  8439  harwdom  8440  infeq5i  8478  cantnfcl  8509  cardiun  8753  infxpenlem  8781  dfac8b  8799  acnnum  8820  inffien  8831  dfac12lem2  8911  cdadom3  8955  cdainflem  8958  cdainf  8959  infunabs  8974  infcda  8975  infdif  8976  infdif2  8977  infmap2  8985  fictb  9012  cofsmo  9036  fin23lem21  9106  hsmexlem1  9193  dmct  9291  mptct  9305  iundomg  9308  iunctb  9341  fpwwe2lem9  9405  canthnum  9416  winalim2  9463  rankcf  9544  tskuni  9550  npomex  9763  hashun2  13109  swrd2lsw  13624  2swrd2eqwrdeq  13625  limsupgord  14132  summolem2  14375  zsum  14377  prodmolem2  14585  zprod  14587  ltoddhalfle  15004  isinv  16336  invsym2  16339  invfun  16340  oppcsect2  16355  oppcinv  16356  efgcpbllemb  18084  frgpuplem  18101  gsumval3  18224  1stcfb  21153  1stcrestlem  21160  2ndcdisj2  21165  txdis1cn  21343  tx1stc  21358  tgphaus  21825  qustgplem  21829  tsmsxp  21863  xmeter  22143  bndth  22660  clmneg1  22785  ovolctb2  23162  ovoliunlem1  23172  i1fd  23349  dvgt0lem2  23665  taylf  24014  efcvx  24102  logccv  24304  loglesqrt  24394  usgredg2v  26006  crctcshtrl  26578  frgr3vlem1  26995  numclwlk1lem2f1  27076  strlem6  28955  mptctf  29329  omsmeas  30158  sibfof  30175  bnj97  30636  bnj553  30668  bnj966  30714  bnj1442  30817  subfaclefac  30858  erdsze2lem1  30885  erdsze2lem2  30886  snmlff  31011  orderseqlem  31442  frrlem5c  31479  bj-ssbid2ALT  32280  phpreu  33011  ptrecube  33027  poimirlem3  33030  poimirlem32  33059  heicant  33062  dvhopellsm  35872  pell1qrgaplem  36903  dnwech  37084  stoweid  39574  dirkercncflem2  39615  fourierdlem36  39654
  Copyright terms: Public domain W3C validator