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  3673  fvsng  7208  fveqf1o  7333  fliftcnv  7342  fliftfun  7343  frxp3  8195  orderseqlem  8201  cnvct  9090  pwdom  9176  php  9250  ordiso  9537  ordtypelem8  9546  wdompwdom  9599  unxpwdom  9610  harwdom  9612  inf0  9649  infeq5i  9664  cantnfcl  9695  cardiun  10090  infxpenlem  10119  acnnum  10158  inffien  10169  dfac12lem2  10250  djudoml  10290  cdainflem  10293  djuinf  10294  infunabs  10311  infdju  10312  infdif  10313  infdif2  10314  infmap2  10322  fictb  10349  cofsmo  10374  fin23lem21  10444  hsmexlem1  10531  dmct  10629  dmctOLD  10630  mptct  10649  iundomg  10652  iunctb  10686  fpwwe2lem8  10750  canthnum  10761  winalim2  10808  rankcf  10889  tskuni  10895  npomex  11108  hashun2  14554  swrd2lsw  15134  2swrd2eqwrdeq  15135  limsupgord  15668  summolem2  15911  zsum  15913  prodmolem2  16131  zprod  16133  ltoddhalfle  16560  isinv  17964  invsym2  17967  invfun  17968  oppcsect2  17983  oppcinv  17984  efgcpbllemb  19999  frgpuplem  20016  gsumval3  20151  1stcfb  23793  1stcrestlem  23800  2ndcdisj2  23806  txdis1cn  23984  tx1stc  23999  tgphaus  24466  qustgplem  24470  tsmsxp  24504  xmeter  24782  bndth  25309  clmneg1  25433  ovolctb2  25843  ovoliunlem1  25853  i1fd  26032  dvgt0lem2  26353  taylf  26718  efcvx  26806  logccv  27021  loglesqrt  27119  0elold  28326  noseqrdgfn  28722  n0fincut  28771  usgredg2v  29838  crctcshtrl  30442  frgr3vlem1  30904  strlem6  32888  mptctf  33379  omsmeas  35025  sibfof  35042  bnj97  35566  bnj553  35598  bnj966  35644  bnj1442  35749  onf1we  35803  weexenwe  35848  tz9.1regs  35902  subfaclefac  36108  erdsze2lem1  36135  erdsze2lem2  36136  snmlff  36261  satffunlem2lem2  36338  bj-ssbid2ALT  37740  phpreu  38719  ptrecube  38730  poimirlem3  38733  poimirlem32  38762  heicant  38765  dvhopellsm  42366  aks5lem7  43442  pell1qrgaplem  44073  dnwech  44248  oaun3lem1  44568  mnurndlem1  45457  hfstructfun  46224  rn1st  46490  stoweid  47278  dirkercncflem2  47319  fourierdlem36  47358  usgrexmpl12ngric  49341  usgrexmpl12ngrlic  49342  elovmpoeq  50185