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  3272  moeq3  3416  reusv1OLD  4897  fveqf1o  6597  fliftcnv  6601  fliftfun  6602  cnvct  8074  undom  8089  pwdom  8153  onomeneq  8191  pwfilem  8301  ordiso  8462  ordtypelem8  8471  wdompwdom  8524  unxpwdom  8535  harwdom  8536  infeq5i  8571  cantnfcl  8602  cardiun  8846  infxpenlem  8874  dfac8b  8892  acnnum  8913  inffien  8924  dfac12lem2  9004  cdadom3  9048  cdainflem  9051  cdainf  9052  infunabs  9067  infcda  9068  infdif  9069  infdif2  9070  infmap2  9078  fictb  9105  cofsmo  9129  fin23lem21  9199  hsmexlem1  9286  dmct  9384  mptct  9398  iundomg  9401  iunctb  9434  fpwwe2lem9  9498  canthnum  9509  winalim2  9556  rankcf  9637  tskuni  9643  npomex  9856  hashun2  13210  swrd2lsw  13741  2swrd2eqwrdeq  13742  limsupgord  14247  summolem2  14491  zsum  14493  prodmolem2  14709  zprod  14711  ltoddhalfle  15132  isinv  16467  invsym2  16470  invfun  16471  oppcsect2  16486  oppcinv  16487  efgcpbllemb  18214  frgpuplem  18231  gsumval3  18354  1stcfb  21296  1stcrestlem  21303  2ndcdisj2  21308  txdis1cn  21486  tx1stc  21501  tgphaus  21967  qustgplem  21971  tsmsxp  22005  xmeter  22285  bndth  22804  clmneg1  22928  ovolctb2  23306  ovoliunlem1  23316  i1fd  23493  dvgt0lem2  23811  taylf  24160  efcvx  24248  logccv  24454  loglesqrt  24544  usgredg2v  26164  crctcshtrl  26771  frgr3vlem1  27253  strlem6  29243  mptctf  29623  omsmeas  30513  sibfof  30530  bnj97  31062  bnj553  31094  bnj966  31140  bnj1442  31243  subfaclefac  31284  erdsze2lem1  31311  erdsze2lem2  31312  snmlff  31437  orderseqlem  31877  frrlem5c  31911  bj-ssbid2ALT  32771  phpreu  33523  ptrecube  33539  poimirlem3  33542  poimirlem32  33571  heicant  33574  dvhopellsm  36723  pell1qrgaplem  37754  dnwech  37935  stoweid  40598  dirkercncflem2  40639  fourierdlem36  40678
  Copyright terms: Public domain W3C validator