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  3670  fvsng  7126  fveqf1o  7248  fliftcnv  7257  fliftfun  7258  frxp3  8093  orderseqlem  8099  cnvct  8971  pwdom  9057  php  9131  ordiso  9421  ordtypelem8  9430  wdompwdom  9483  unxpwdom  9494  harwdom  9496  inf0  9530  infeq5i  9545  cantnfcl  9576  cardiun  9894  infxpenlem  9923  dfac8b  9941  acnnum  9962  inffien  9973  dfac12lem2  10055  djudoml  10095  cdainflem  10098  djuinf  10099  infunabs  10116  infdju  10117  infdif  10118  infdif2  10119  infmap2  10127  fictb  10154  cofsmo  10179  fin23lem21  10249  hsmexlem1  10336  dmct  10434  mptct  10448  iundomg  10451  iunctb  10485  fpwwe2lem8  10549  canthnum  10560  winalim2  10607  rankcf  10688  tskuni  10694  npomex  10907  hashun2  14306  swrd2lsw  14875  2swrd2eqwrdeq  14876  limsupgord  15395  summolem2  15639  zsum  15641  prodmolem2  15858  zprod  15860  ltoddhalfle  16288  isinv  17684  invsym2  17687  invfun  17688  oppcsect2  17703  oppcinv  17704  efgcpbllemb  19684  frgpuplem  19701  gsumval3  19836  1stcfb  23389  1stcrestlem  23396  2ndcdisj2  23401  txdis1cn  23579  tx1stc  23594  tgphaus  24061  qustgplem  24065  tsmsxp  24099  xmeter  24377  bndth  24913  clmneg1  25038  ovolctb2  25449  ovoliunlem1  25459  i1fd  25638  dvgt0lem2  25964  taylf  26324  efcvx  26415  logccv  26628  loglesqrt  26727  0elold  27906  noseqrdgfn  28302  n0fincut  28351  usgredg2v  29300  crctcshtrl  29896  frgr3vlem1  30348  strlem6  32331  mptctf  32795  omsmeas  34480  sibfof  34497  bnj97  35022  bnj553  35054  bnj966  35100  bnj1442  35205  tz9.1regs  35290  subfaclefac  35370  erdsze2lem1  35397  erdsze2lem2  35398  snmlff  35523  satffunlem2lem2  35600  bj-ssbid2ALT  36864  phpreu  37801  ptrecube  37817  poimirlem3  37820  poimirlem32  37849  heicant  37852  dvhopellsm  41373  aks5lem7  42450  pell1qrgaplem  43111  dnwech  43286  oaun3lem1  43612  mnurndlem1  44518  rn1st  45513  stoweid  46303  dirkercncflem2  46344  fourierdlem36  46383  usgrexmpl12ngric  48280  usgrexmpl12ngrlic  48281