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:  ceqsexOLD  3528  ceqsexvOLD  3530  moeq3  3720  fvsng  7199  fveqf1o  7321  fliftcnv  7330  fliftfun  7331  frxp3  8174  orderseqlem  8180  cnvct  9072  undomOLD  9098  pwdom  9167  php  9244  onomeneqOLD  9263  ordiso  9553  ordtypelem8  9562  wdompwdom  9615  unxpwdom  9626  harwdom  9628  inf0  9658  infeq5i  9673  cantnfcl  9704  cardiun  10019  infxpenlem  10050  dfac8b  10068  acnnum  10089  inffien  10100  dfac12lem2  10182  djudoml  10222  cdainflem  10225  djuinf  10226  infunabs  10243  infdju  10244  infdif  10245  infdif2  10246  infmap2  10254  fictb  10281  cofsmo  10306  fin23lem21  10376  hsmexlem1  10463  dmct  10561  mptct  10575  iundomg  10578  iunctb  10611  fpwwe2lem8  10675  canthnum  10686  winalim2  10733  rankcf  10814  tskuni  10820  npomex  11033  hashun2  14418  swrd2lsw  14987  2swrd2eqwrdeq  14988  limsupgord  15504  summolem2  15748  zsum  15750  prodmolem2  15967  zprod  15969  ltoddhalfle  16394  isinv  17807  invsym2  17810  invfun  17811  oppcsect2  17826  oppcinv  17827  efgcpbllemb  19787  frgpuplem  19804  gsumval3  19939  1stcfb  23468  1stcrestlem  23475  2ndcdisj2  23480  txdis1cn  23658  tx1stc  23673  tgphaus  24140  qustgplem  24144  tsmsxp  24178  xmeter  24458  bndth  25003  clmneg1  25128  ovolctb2  25540  ovoliunlem1  25550  i1fd  25729  dvgt0lem2  26056  taylf  26416  efcvx  26507  logccv  26719  loglesqrt  26818  0elold  27961  noseqrdgfn  28326  usgredg2v  29258  crctcshtrl  29852  frgr3vlem1  30301  strlem6  32284  mptctf  32734  omsmeas  34304  sibfof  34321  bnj97  34858  bnj553  34890  bnj966  34936  bnj1442  35041  subfaclefac  35160  erdsze2lem1  35187  erdsze2lem2  35188  snmlff  35313  satffunlem2lem2  35390  bj-ssbid2ALT  36645  phpreu  37590  ptrecube  37606  poimirlem3  37609  poimirlem32  37638  heicant  37641  dvhopellsm  41099  aks5lem7  42181  pell1qrgaplem  42860  dnwech  43036  oaun3lem1  43363  mnurndlem1  44276  rn1st  45218  stoweid  46018  dirkercncflem2  46059  fourierdlem36  46098  usgrexmpl12ngric  47932  usgrexmpl12ngrlic  47933