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  3515  moeq3  3700  fvsng  7177  fveqf1o  7300  fliftcnv  7309  fliftfun  7310  frxp3  8155  orderseqlem  8161  cnvct  9053  undomOLD  9079  pwdom  9148  php  9226  onomeneqOLD  9243  ordiso  9535  ordtypelem8  9544  wdompwdom  9597  unxpwdom  9608  harwdom  9610  inf0  9640  infeq5i  9655  cantnfcl  9686  cardiun  10001  infxpenlem  10032  dfac8b  10050  acnnum  10071  inffien  10082  dfac12lem2  10164  djudoml  10204  cdainflem  10207  djuinf  10208  infunabs  10225  infdju  10226  infdif  10227  infdif2  10228  infmap2  10236  fictb  10263  cofsmo  10288  fin23lem21  10358  hsmexlem1  10445  dmct  10543  mptct  10557  iundomg  10560  iunctb  10593  fpwwe2lem8  10657  canthnum  10668  winalim2  10715  rankcf  10796  tskuni  10802  npomex  11015  hashun2  14406  swrd2lsw  14976  2swrd2eqwrdeq  14977  limsupgord  15493  summolem2  15737  zsum  15739  prodmolem2  15956  zprod  15958  ltoddhalfle  16385  isinv  17778  invsym2  17781  invfun  17782  oppcsect2  17797  oppcinv  17798  efgcpbllemb  19741  frgpuplem  19758  gsumval3  19893  1stcfb  23388  1stcrestlem  23395  2ndcdisj2  23400  txdis1cn  23578  tx1stc  23593  tgphaus  24060  qustgplem  24064  tsmsxp  24098  xmeter  24377  bndth  24913  clmneg1  25038  ovolctb2  25450  ovoliunlem1  25460  i1fd  25639  dvgt0lem2  25965  taylf  26325  efcvx  26416  logccv  26629  loglesqrt  26728  0elold  27878  noseqrdgfn  28257  n0sfincut  28303  usgredg2v  29211  crctcshtrl  29810  frgr3vlem1  30259  strlem6  32242  mptctf  32700  omsmeas  34360  sibfof  34377  bnj97  34902  bnj553  34934  bnj966  34980  bnj1442  35085  subfaclefac  35203  erdsze2lem1  35230  erdsze2lem2  35231  snmlff  35356  satffunlem2lem2  35433  bj-ssbid2ALT  36686  phpreu  37633  ptrecube  37649  poimirlem3  37652  poimirlem32  37681  heicant  37684  dvhopellsm  41141  aks5lem7  42218  pell1qrgaplem  42871  dnwech  43047  oaun3lem1  43373  mnurndlem1  44280  rn1st  45277  stoweid  46072  dirkercncflem2  46113  fourierdlem36  46152  usgrexmpl12ngric  48022  usgrexmpl12ngrlic  48023