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:  ceqsexOLD  3541  ceqsexvOLD  3543  moeq3  3734  fvsng  7214  fveqf1o  7338  fliftcnv  7347  fliftfun  7348  frxp3  8192  orderseqlem  8198  cnvct  9099  undomOLD  9126  pwdom  9195  php  9273  onomeneqOLD  9292  pwfilemOLD  9416  ordiso  9585  ordtypelem8  9594  wdompwdom  9647  unxpwdom  9658  harwdom  9660  inf0  9690  infeq5i  9705  cantnfcl  9736  cardiun  10051  infxpenlem  10082  dfac8b  10100  acnnum  10121  inffien  10132  dfac12lem2  10214  djudoml  10254  cdainflem  10257  djuinf  10258  infunabs  10275  infdju  10276  infdif  10277  infdif2  10278  infmap2  10286  fictb  10313  cofsmo  10338  fin23lem21  10408  hsmexlem1  10495  dmct  10593  mptct  10607  iundomg  10610  iunctb  10643  fpwwe2lem8  10707  canthnum  10718  winalim2  10765  rankcf  10846  tskuni  10852  npomex  11065  hashun2  14432  swrd2lsw  15001  2swrd2eqwrdeq  15002  limsupgord  15518  summolem2  15764  zsum  15766  prodmolem2  15983  zprod  15985  ltoddhalfle  16409  isinv  17821  invsym2  17824  invfun  17825  oppcsect2  17840  oppcinv  17841  efgcpbllemb  19797  frgpuplem  19814  gsumval3  19949  1stcfb  23474  1stcrestlem  23481  2ndcdisj2  23486  txdis1cn  23664  tx1stc  23679  tgphaus  24146  qustgplem  24150  tsmsxp  24184  xmeter  24464  bndth  25009  clmneg1  25134  ovolctb2  25546  ovoliunlem1  25556  i1fd  25735  dvgt0lem2  26062  taylf  26420  efcvx  26511  logccv  26723  loglesqrt  26822  0elold  27965  noseqrdgfn  28330  usgredg2v  29262  crctcshtrl  29856  frgr3vlem1  30305  strlem6  32288  mptctf  32731  omsmeas  34288  sibfof  34305  bnj97  34842  bnj553  34874  bnj966  34920  bnj1442  35025  subfaclefac  35144  erdsze2lem1  35171  erdsze2lem2  35172  snmlff  35297  satffunlem2lem2  35374  bj-ssbid2ALT  36629  phpreu  37564  ptrecube  37580  poimirlem3  37583  poimirlem32  37612  heicant  37615  dvhopellsm  41074  aks5lem7  42157  pell1qrgaplem  42829  dnwech  43005  oaun3lem1  43336  mnurndlem1  44250  rn1st  45183  stoweid  45984  dirkercncflem2  46025  fourierdlem36  46064  usgrexmpl12ngric  47853  usgrexmpl12ngrlic  47854