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

Step	Hyp	Ref	Expression
1		mpisyl.1	. 2 ⊢ (𝜑 → 𝜓)
2		mpisyl.2	. . 3 ⊢ 𝜒
3		mpisyl.3	. . 3 ⊢ (𝜓 → (𝜒 → 𝜃))
4	2, 3	mpi 20	. 2 ⊢ (𝜓 → 𝜃)
5	1, 4	syl 17	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  moeq3  3658  fvsng  7135  fveqf1o  7257  fliftcnv  7266  fliftfun  7267  frxp3  8101  orderseqlem  8107  cnvct  8981  pwdom  9067  php  9141  ordiso  9431  ordtypelem8  9440  wdompwdom  9493  unxpwdom  9504  harwdom  9506  inf0  9542  infeq5i  9557  cantnfcl  9588  cardiun  9906  infxpenlem  9935  dfac8b  9953  acnnum  9974  inffien  9985  dfac12lem2  10067  djudoml  10107  cdainflem  10110  djuinf  10111  infunabs  10128  infdju  10129  infdif  10130  infdif2  10131  infmap2  10139  fictb  10166  cofsmo  10191  fin23lem21  10261  hsmexlem1  10348  dmct  10446  mptct  10460  iundomg  10463  iunctb  10497  fpwwe2lem8  10561  canthnum  10572  winalim2  10619  rankcf  10700  tskuni  10706  npomex  10919  hashun2  14345  swrd2lsw  14914  2swrd2eqwrdeq  14915  limsupgord  15434  summolem2  15678  zsum  15680  prodmolem2  15900  zprod  15902  ltoddhalfle  16330  isinv  17727  invsym2  17730  invfun  17731  oppcsect2  17746  oppcinv  17747  efgcpbllemb  19730  frgpuplem  19747  gsumval3  19882  1stcfb  23410  1stcrestlem  23417  2ndcdisj2  23422  txdis1cn  23600  tx1stc  23615  tgphaus  24082  qustgplem  24086  tsmsxp  24120  xmeter  24398  bndth  24925  clmneg1  25049  ovolctb2  25459  ovoliunlem1  25469  i1fd  25648  dvgt0lem2  25970  taylf  26326  efcvx  26414  logccv  26627  loglesqrt  26725  0elold  27902  noseqrdgfn  28298  n0fincut  28347  usgredg2v  29296  crctcshtrl  29891  frgr3vlem1  30343  strlem6  32327  mptctf  32789  omsmeas  34467  sibfof  34484  bnj97  35008  bnj553  35040  bnj966  35086  bnj1442  35191  tz9.1regs  35278  subfaclefac  35358  erdsze2lem1  35385  erdsze2lem2  35386  snmlff  35511  satffunlem2lem2  35588  bj-ssbid2ALT  36957  phpreu  37925  ptrecube  37941  poimirlem3  37944  poimirlem32  37973  heicant  37976  dvhopellsm  41563  aks5lem7  42639  pell1qrgaplem  43301  dnwech  43476  oaun3lem1  43802  mnurndlem1  44708  rn1st  45702  stoweid  46491  dirkercncflem2  46532  fourierdlem36  46571  usgrexmpl12ngric  48514  usgrexmpl12ngrlic  48515