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  3670  fvsng  7177  fveqf1o  7302  fliftcnv  7311  fliftfun  7312  frxp3  8152  orderseqlem  8158  cnvct  9046  pwdom  9132  php  9206  ordiso  9494  ordtypelem8  9503  wdompwdom  9556  unxpwdom  9567  harwdom  9569  inf0  9606  infeq5i  9621  cantnfcl  9652  cardiun  10044  infxpenlem  10073  acnnum  10112  inffien  10123  dfac12lem2  10204  djudoml  10244  cdainflem  10247  djuinf  10248  infunabs  10265  infdju  10266  infdif  10267  infdif2  10268  infmap2  10276  fictb  10303  cofsmo  10328  fin23lem21  10398  hsmexlem1  10485  dmct  10583  dmctOLD  10584  mptct  10603  iundomg  10606  iunctb  10640  fpwwe2lem8  10704  canthnum  10715  winalim2  10762  rankcf  10843  tskuni  10849  npomex  11062  hashun2  14507  swrd2lsw  15085  2swrd2eqwrdeq  15086  limsupgord  15619  summolem2  15862  zsum  15864  prodmolem2  16082  zprod  16084  ltoddhalfle  16511  isinv  17915  invsym2  17918  invfun  17919  oppcsect2  17934  oppcinv  17935  efgcpbllemb  19949  frgpuplem  19966  gsumval3  20101  1stcfb  23743  1stcrestlem  23750  2ndcdisj2  23756  txdis1cn  23934  tx1stc  23949  tgphaus  24416  qustgplem  24420  tsmsxp  24454  xmeter  24732  bndth  25259  clmneg1  25383  ovolctb2  25793  ovoliunlem1  25803  i1fd  25982  dvgt0lem2  26303  taylf  26670  efcvx  26758  logccv  26973  loglesqrt  27071  0elold  28278  noseqrdgfn  28674  n0fincut  28723  usgredg2v  29790  crctcshtrl  30394  frgr3vlem1  30856  strlem6  32840  mptctf  33290  omsmeas  34938  sibfof  34955  bnj97  35479  bnj553  35511  bnj966  35557  bnj1442  35662  tz9.1regs  35775  subfaclefac  35910  erdsze2lem1  35937  erdsze2lem2  35938  snmlff  36063  satffunlem2lem2  36140  bj-ssbid2ALT  37532  phpreu  38495  ptrecube  38506  poimirlem3  38509  poimirlem32  38538  heicant  38541  dvhopellsm  42142  aks5lem7  43218  pell1qrgaplem  43833  dnwech  44008  oaun3lem1  44334  mnurndlem1  45224  rn1st  46228  stoweid  47017  dirkercncflem2  47058  fourierdlem36  47097  usgrexmpl12ngric  49080  usgrexmpl12ngrlic  49081