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  14212  swrd2lsw  14774  2swrd2eqwrdeq  14775  limsupgord  15290  summolem2  15537  zsum  15539  prodmolem2  15754  zprod  15756  ltoddhalfle  16179  isinv  17579  invsym2  17582  invfun  17583  oppcsect2  17598  oppcinv  17599  efgcpbllemb  19472  frgpuplem  19489  gsumval3  19619  1stcfb  22724  1stcrestlem  22731  2ndcdisj2  22736  txdis1cn  22914  tx1stc  22929  tgphaus  23396  qustgplem  23400  tsmsxp  23434  xmeter  23714  bndth  24249  clmneg1  24373  ovolctb2  24784  ovoliunlem1  24794  i1fd  24973  dvgt0lem2  25295  taylf  25648  efcvx  25736  logccv  25946  loglesqrt  26039  usgredg2v  27980  crctcshtrl  28573  frgr3vlem1  29022  strlem6  31003  mptctf  31435  omsmeas  32703  sibfof  32720  bnj97  33258  bnj553  33290  bnj966  33336  bnj1442  33441  subfaclefac  33550  erdsze2lem1  33577  erdsze2lem2  33578  snmlff  33703  satffunlem2lem2  33780  frxp3  34189  bj-ssbid2ALT  35058  phpreu  35993  ptrecube  36009  poimirlem3  36012  poimirlem32  36041  heicant  36044  dvhopellsm  39511  pell1qrgaplem  41098  dnwech  41277  mnurndlem1  42362  rn1st  43298  stoweid  44095  dirkercncflem2  44136  fourierdlem36  44175
  Copyright terms: Public domain W3C validator