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  3479  ceqsexv  3480  moeq3  3648  fvsng  7061  fveqf1o  7184  fliftcnv  7191  fliftfun  7192  cnvct  8833  undomOLD  8856  pwdom  8925  php  9002  onomeneqOLD  9021  pwfilemOLD  9122  ordiso  9284  ordtypelem8  9293  wdompwdom  9346  unxpwdom  9357  harwdom  9359  inf0  9388  infeq5i  9403  cantnfcl  9434  cardiun  9749  infxpenlem  9778  dfac8b  9796  acnnum  9817  inffien  9828  dfac12lem2  9909  djudoml  9949  cdainflem  9952  djuinf  9953  infunabs  9972  infdju  9973  infdif  9974  infdif2  9975  infmap2  9983  fictb  10010  cofsmo  10034  fin23lem21  10104  hsmexlem1  10191  dmct  10289  mptct  10303  iundomg  10306  iunctb  10339  fpwwe2lem8  10403  canthnum  10414  winalim2  10461  rankcf  10542  tskuni  10548  npomex  10761  hashun2  14107  swrd2lsw  14674  2swrd2eqwrdeq  14675  limsupgord  15190  summolem2  15437  zsum  15439  prodmolem2  15654  zprod  15656  ltoddhalfle  16079  isinv  17481  invsym2  17484  invfun  17485  oppcsect2  17500  oppcinv  17501  efgcpbllemb  19370  frgpuplem  19387  gsumval3  19517  1stcfb  22605  1stcrestlem  22612  2ndcdisj2  22617  txdis1cn  22795  tx1stc  22810  tgphaus  23277  qustgplem  23281  tsmsxp  23315  xmeter  23595  bndth  24130  clmneg1  24254  ovolctb2  24665  ovoliunlem1  24675  i1fd  24854  dvgt0lem2  25176  taylf  25529  efcvx  25617  logccv  25827  loglesqrt  25920  usgredg2v  27603  crctcshtrl  28197  frgr3vlem1  28646  strlem6  30627  mptctf  31061  omsmeas  32299  sibfof  32316  bnj97  32855  bnj553  32887  bnj966  32933  bnj1442  33038  subfaclefac  33147  erdsze2lem1  33174  erdsze2lem2  33175  snmlff  33300  satffunlem2lem2  33377  frxp3  33806  orderseqlem  33810  bj-ssbid2ALT  34853  phpreu  35770  ptrecube  35786  poimirlem3  35789  poimirlem32  35818  heicant  35821  dvhopellsm  39138  pell1qrgaplem  40702  dnwech  40880  mnurndlem1  41906  stoweid  43611  dirkercncflem2  43652  fourierdlem36  43691