Theorem mpisyl 22

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 21	. 2 ⊢ (𝜓 → 𝜃)
5	1, 4	syl 18	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  3676  fvsng  7180  fveqf1o  7302  fliftcnv  7311  fliftfun  7312  frxp3  8148  orderseqlem  8154  cnvct  9032  pwdom  9118  php  9192  ordiso  9479  ordtypelem8  9488  wdompwdom  9541  unxpwdom  9552  harwdom  9554  inf0  9591  infeq5i  9606  cantnfcl  9637  cardiun  9969  infxpenlem  9998  dfac8b  10016  acnnum  10037  inffien  10048  dfac12lem2  10129  djudoml  10169  cdainflem  10172  djuinf  10173  infunabs  10190  infdju  10191  infdif  10192  infdif2  10193  infmap2  10201  fictb  10228  cofsmo  10254  fin23lem21  10324  hsmexlem1  10411  dmct  10509  mptct  10523  iundomg  10526  iunctb  10560  fpwwe2lem8  10624  canthnum  10635  winalim2  10682  rankcf  10763  tskuni  10769  npomex  10982  hashun2  14421  swrd2lsw  14991  2swrd2eqwrdeq  14992  limsupgord  15525  summolem2  15769  zsum  15771  prodmolem2  15991  zprod  15993  ltoddhalfle  16420  isinv  17818  invsym2  17821  invfun  17822  oppcsect2  17837  oppcinv  17838  efgcpbllemb  19826  frgpuplem  19843  gsumval3  19978  1stcfb  23583  1stcrestlem  23590  2ndcdisj2  23595  txdis1cn  23773  tx1stc  23788  tgphaus  24255  qustgplem  24259  tsmsxp  24293  xmeter  24571  bndth  25098  clmneg1  25222  ovolctb2  25632  ovoliunlem1  25642  i1fd  25821  dvgt0lem2  26143  taylf  26502  efcvx  26590  logccv  26806  loglesqrt  26904  0elold  28081  noseqrdgfn  28477  n0fincut  28526  usgredg2v  29555  crctcshtrl  30150  frgr3vlem1  30602  strlem6  32586  mptctf  33039  omsmeas  34691  sibfof  34708  bnj97  35232  bnj553  35264  bnj966  35310  bnj1442  35415  tz9.1regs  35525  subfaclefac  35646  erdsze2lem1  35673  erdsze2lem2  35674  snmlff  35799  satffunlem2lem2  35876  bj-ssbid2ALT  37263  phpreu  38233  ptrecube  38249  poimirlem3  38252  poimirlem32  38281  heicant  38284  dvhopellsm  41869  aks5lem7  42945  pell1qrgaplem  43580  dnwech  43755  oaun3lem1  44081  mnurndlem1  44971  rn1st  45968  stoweid  46757  dirkercncflem2  46798  fourierdlem36  46837  usgrexmpl12ngric  48780  usgrexmpl12ngrlic  48781