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 ⊢ (𝜑 → 𝜃)

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  moeq3  3669  fvsng  7185  fveqf1o  7310  fliftcnv  7319  fliftfun  7320  frxp3  8170  orderseqlem  8176  cnvct  9065  pwdom  9151  php  9225  ordiso  9513  ordtypelem8  9522  wdompwdom  9575  unxpwdom  9586  harwdom  9588  inf0  9625  infeq5i  9640  cantnfcl  9671  cardiun  10066  infxpenlem  10095  acnnum  10134  inffien  10145  dfac12lem2  10226  djudoml  10266  cdainflem  10269  djuinf  10270  infunabs  10287  infdju  10288  infdif  10289  infdif2  10290  infmap2  10298  fictb  10325  cofsmo  10350  fin23lem21  10420  hsmexlem1  10507  dmct  10605  dmctOLD  10606  mptct  10625  iundomg  10628  iunctb  10662  fpwwe2lem8  10726  canthnum  10737  winalim2  10784  rankcf  10865  tskuni  10871  npomex  11084  hashun2  14530  swrd2lsw  15110  2swrd2eqwrdeq  15111  limsupgord  15644  summolem2  15887  zsum  15889  prodmolem2  16107  zprod  16109  ltoddhalfle  16536  isinv  17940  invsym2  17943  invfun  17944  oppcsect2  17959  oppcinv  17960  efgcpbllemb  19974  frgpuplem  19991  gsumval3  20126  1stcfb  23768  1stcrestlem  23775  2ndcdisj2  23781  txdis1cn  23959  tx1stc  23974  tgphaus  24441  qustgplem  24445  tsmsxp  24479  xmeter  24757  bndth  25284  clmneg1  25408  ovolctb2  25818  ovoliunlem1  25828  i1fd  26007  dvgt0lem2  26328  taylf  26693  efcvx  26781  logccv  26996  loglesqrt  27094  0elold  28301  noseqrdgfn  28697  n0fincut  28746  usgredg2v  29813  crctcshtrl  30417  frgr3vlem1  30879  strlem6  32863  mptctf  33355  omsmeas  35001  sibfof  35018  bnj97  35542  bnj553  35574  bnj966  35620  bnj1442  35725  onf1we  35771  weexenwe  35812  tz9.1regs  35858  subfaclefac  36027  erdsze2lem1  36054  erdsze2lem2  36055  snmlff  36180  satffunlem2lem2  36257  bj-ssbid2ALT  37654  phpreu  38620  ptrecube  38631  poimirlem3  38634  poimirlem32  38663  heicant  38666  dvhopellsm  42267  aks5lem7  43343  pell1qrgaplem  43973  dnwech  44148  oaun3lem1  44469  mnurndlem1  45358  hfstructfun  46119  rn1st  46378  stoweid  47166  dirkercncflem2  47207  fourierdlem36  47246  usgrexmpl12ngric  49229  usgrexmpl12ngrlic  49230  elovmpoeq  50073