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  3491  moeq3  3654  fvsng  6923  fveqf1o  7041  fliftcnv  7047  fliftfun  7048  cnvct  8573  undom  8592  pwdom  8657  onomeneq  8697  pwfilem  8806  ordiso  8968  ordtypelem8  8977  wdompwdom  9030  unxpwdom  9041  harwdom  9043  inf0  9072  infeq5i  9087  cantnfcl  9118  cardiun  9399  infxpenlem  9428  dfac8b  9446  acnnum  9467  inffien  9478  dfac12lem2  9559  djudoml  9599  cdainflem  9602  djuinf  9603  infunabs  9622  infdju  9623  infdif  9624  infdif2  9625  infmap2  9633  fictb  9660  cofsmo  9684  fin23lem21  9754  hsmexlem1  9841  dmct  9939  mptct  9953  iundomg  9956  iunctb  9989  fpwwe2lem9  10053  canthnum  10064  winalim2  10111  rankcf  10192  tskuni  10198  npomex  10411  hashun2  13744  swrd2lsw  14309  2swrd2eqwrdeq  14310  limsupgord  14824  summolem2  15068  zsum  15070  prodmolem2  15284  zprod  15286  ltoddhalfle  15705  isinv  17025  invsym2  17028  invfun  17029  oppcsect2  17044  oppcinv  17045  efgcpbllemb  18876  frgpuplem  18893  gsumval3  19023  1stcfb  22053  1stcrestlem  22060  2ndcdisj2  22065  txdis1cn  22243  tx1stc  22258  tgphaus  22725  qustgplem  22729  tsmsxp  22763  xmeter  23043  bndth  23566  clmneg1  23690  ovolctb2  24099  ovoliunlem1  24109  i1fd  24288  dvgt0lem2  24609  taylf  24959  efcvx  25047  logccv  25257  loglesqrt  25350  usgredg2v  27020  crctcshtrl  27612  frgr3vlem1  28061  strlem6  30042  mptctf  30482  omsmeas  31689  sibfof  31706  bnj97  32246  bnj553  32278  bnj966  32324  bnj1442  32429  subfaclefac  32531  erdsze2lem1  32558  erdsze2lem2  32559  snmlff  32684  satffunlem2lem2  32761  orderseqlem  33202  bj-ssbid2ALT  34104  phpreu  35034  ptrecube  35050  poimirlem3  35053  poimirlem32  35082  heicant  35085  dvhopellsm  38406  pell1qrgaplem  39801  dnwech  39979  mnurndlem1  40976  stoweid  42692  dirkercncflem2  42733  fourierdlem36  42772
  Copyright terms: Public domain W3C validator