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:  ceqsex  3444  ceqsexv  3445  moeq3  3614  fvsng  6973  fveqf1o  7091  fliftcnv  7098  fliftfun  7099  cnvct  8689  undom  8711  pwdom  8776  onomeneq  8845  pwfilemOLD  8948  ordiso  9110  ordtypelem8  9119  wdompwdom  9172  unxpwdom  9183  harwdom  9185  inf0  9214  infeq5i  9229  cantnfcl  9260  cardiun  9563  infxpenlem  9592  dfac8b  9610  acnnum  9631  inffien  9642  dfac12lem2  9723  djudoml  9763  cdainflem  9766  djuinf  9767  infunabs  9786  infdju  9787  infdif  9788  infdif2  9789  infmap2  9797  fictb  9824  cofsmo  9848  fin23lem21  9918  hsmexlem1  10005  dmct  10103  mptct  10117  iundomg  10120  iunctb  10153  fpwwe2lem8  10217  canthnum  10228  winalim2  10275  rankcf  10356  tskuni  10362  npomex  10575  hashun2  13915  swrd2lsw  14482  2swrd2eqwrdeq  14483  limsupgord  14998  summolem2  15245  zsum  15247  prodmolem2  15460  zprod  15462  ltoddhalfle  15885  isinv  17219  invsym2  17222  invfun  17223  oppcsect2  17238  oppcinv  17239  efgcpbllemb  19099  frgpuplem  19116  gsumval3  19246  1stcfb  22296  1stcrestlem  22303  2ndcdisj2  22308  txdis1cn  22486  tx1stc  22501  tgphaus  22968  qustgplem  22972  tsmsxp  23006  xmeter  23285  bndth  23809  clmneg1  23933  ovolctb2  24343  ovoliunlem1  24353  i1fd  24532  dvgt0lem2  24854  taylf  25207  efcvx  25295  logccv  25505  loglesqrt  25598  usgredg2v  27269  crctcshtrl  27861  frgr3vlem1  28310  strlem6  30291  mptctf  30726  omsmeas  31956  sibfof  31973  bnj97  32513  bnj553  32545  bnj966  32591  bnj1442  32696  subfaclefac  32805  erdsze2lem1  32832  erdsze2lem2  32833  snmlff  32958  satffunlem2lem2  33035  frxp3  33477  orderseqlem  33481  bj-ssbid2ALT  34530  phpreu  35447  ptrecube  35463  poimirlem3  35466  poimirlem32  35495  heicant  35498  dvhopellsm  38817  pell1qrgaplem  40339  dnwech  40517  mnurndlem1  41513  stoweid  43222  dirkercncflem2  43263  fourierdlem36  43302