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  3538  moeq3  3700  fvsng  6934  fveqf1o  7049  fliftcnv  7053  fliftfun  7054  cnvct  8574  undom  8593  pwdom  8657  onomeneq  8696  pwfilem  8806  ordiso  8968  ordtypelem8  8977  wdompwdom  9030  unxpwdom  9041  harwdom  9042  infeq5i  9087  cantnfcl  9118  cardiun  9399  infxpenlem  9427  dfac8b  9445  acnnum  9466  inffien  9477  dfac12lem2  9558  djudoml  9598  cdainflem  9601  djuinf  9602  infunabs  9617  infdju  9618  infdif  9619  infdif2  9620  infmap2  9628  fictb  9655  cofsmo  9679  fin23lem21  9749  hsmexlem1  9836  dmct  9934  mptct  9948  iundomg  9951  iunctb  9984  fpwwe2lem9  10048  canthnum  10059  winalim2  10106  rankcf  10187  tskuni  10193  npomex  10406  hashun2  13732  swrd2lsw  14302  2swrd2eqwrdeq  14303  limsupgord  14817  summolem2  15061  zsum  15063  prodmolem2  15277  zprod  15279  ltoddhalfle  15698  isinv  17018  invsym2  17021  invfun  17022  oppcsect2  17037  oppcinv  17038  efgcpbllemb  18810  frgpuplem  18827  gsumval3  18956  1stcfb  21981  1stcrestlem  21988  2ndcdisj2  21993  txdis1cn  22171  tx1stc  22186  tgphaus  22652  qustgplem  22656  tsmsxp  22690  xmeter  22970  bndth  23489  clmneg1  23613  ovolctb2  24020  ovoliunlem1  24030  i1fd  24209  dvgt0lem2  24527  taylf  24876  efcvx  24964  logccv  25173  loglesqrt  25266  usgredg2v  26936  crctcshtrl  27528  frgr3vlem1  27979  strlem6  29960  mptctf  30379  omsmeas  31480  sibfof  31497  bnj97  32037  bnj553  32069  bnj966  32115  bnj1442  32218  subfaclefac  32320  erdsze2lem1  32347  erdsze2lem2  32348  snmlff  32473  satffunlem2lem2  32550  orderseqlem  32991  bj-ssbid2ALT  33893  phpreu  34757  ptrecube  34773  poimirlem3  34776  poimirlem32  34805  heicant  34808  dvhopellsm  38133  pell1qrgaplem  39348  dnwech  39526  mnurndlem1  40494  stoweid  42225  dirkercncflem2  42266  fourierdlem36  42305
  Copyright terms: Public domain W3C validator