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:  ceqsexOLD  3492  ceqsexvOLD  3494  moeq3  3669  fvsng  7121  fveqf1o  7244  fliftcnv  7251  fliftfun  7252  orderseqlem  8057  cnvct  8912  undomOLD  8938  pwdom  9007  php  9088  onomeneqOLD  9107  pwfilemOLD  9224  ordiso  9386  ordtypelem8  9395  wdompwdom  9448  unxpwdom  9459  harwdom  9461  inf0  9491  infeq5i  9506  cantnfcl  9537  cardiun  9852  infxpenlem  9883  dfac8b  9901  acnnum  9922  inffien  9933  dfac12lem2  10014  djudoml  10054  cdainflem  10057  djuinf  10058  infunabs  10077  infdju  10078  infdif  10079  infdif2  10080  infmap2  10088  fictb  10115  cofsmo  10139  fin23lem21  10209  hsmexlem1  10296  dmct  10394  mptct  10408  iundomg  10411  iunctb  10444  fpwwe2lem8  10508  canthnum  10519  winalim2  10566  rankcf  10647  tskuni  10653  npomex  10866  hashun2  14211  swrd2lsw  14773  2swrd2eqwrdeq  14774  limsupgord  15289  summolem2  15536  zsum  15538  prodmolem2  15753  zprod  15755  ltoddhalfle  16178  isinv  17578  invsym2  17581  invfun  17582  oppcsect2  17597  oppcinv  17598  efgcpbllemb  19467  frgpuplem  19484  gsumval3  19614  1stcfb  22719  1stcrestlem  22726  2ndcdisj2  22731  txdis1cn  22909  tx1stc  22924  tgphaus  23391  qustgplem  23395  tsmsxp  23429  xmeter  23709  bndth  24244  clmneg1  24368  ovolctb2  24779  ovoliunlem1  24789  i1fd  24968  dvgt0lem2  25290  taylf  25643  efcvx  25731  logccv  25941  loglesqrt  26034  usgredg2v  27974  crctcshtrl  28567  frgr3vlem1  29016  strlem6  30997  mptctf  31429  omsmeas  32697  sibfof  32714  bnj97  33252  bnj553  33284  bnj966  33330  bnj1442  33435  subfaclefac  33544  erdsze2lem1  33571  erdsze2lem2  33572  snmlff  33697  satffunlem2lem2  33774  frxp3  34186  bj-ssbid2ALT  35023  phpreu  35958  ptrecube  35974  poimirlem3  35977  poimirlem32  36006  heicant  36009  dvhopellsm  39476  pell1qrgaplem  41062  dnwech  41241  mnurndlem1  42326  rn1st  43262  stoweid  44059  dirkercncflem2  44100  fourierdlem36  44139
  Copyright terms: Public domain W3C validator