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  3531  moeq3  3718  fvsng  7200  fveqf1o  7322  fliftcnv  7331  fliftfun  7332  frxp3  8176  orderseqlem  8182  cnvct  9074  undomOLD  9100  pwdom  9169  php  9247  onomeneqOLD  9266  ordiso  9556  ordtypelem8  9565  wdompwdom  9618  unxpwdom  9629  harwdom  9631  inf0  9661  infeq5i  9676  cantnfcl  9707  cardiun  10022  infxpenlem  10053  dfac8b  10071  acnnum  10092  inffien  10103  dfac12lem2  10185  djudoml  10225  cdainflem  10228  djuinf  10229  infunabs  10246  infdju  10247  infdif  10248  infdif2  10249  infmap2  10257  fictb  10284  cofsmo  10309  fin23lem21  10379  hsmexlem1  10466  dmct  10564  mptct  10578  iundomg  10581  iunctb  10614  fpwwe2lem8  10678  canthnum  10689  winalim2  10736  rankcf  10817  tskuni  10823  npomex  11036  hashun2  14422  swrd2lsw  14991  2swrd2eqwrdeq  14992  limsupgord  15508  summolem2  15752  zsum  15754  prodmolem2  15971  zprod  15973  ltoddhalfle  16398  isinv  17804  invsym2  17807  invfun  17808  oppcsect2  17823  oppcinv  17824  efgcpbllemb  19773  frgpuplem  19790  gsumval3  19925  1stcfb  23453  1stcrestlem  23460  2ndcdisj2  23465  txdis1cn  23643  tx1stc  23658  tgphaus  24125  qustgplem  24129  tsmsxp  24163  xmeter  24443  bndth  24990  clmneg1  25115  ovolctb2  25527  ovoliunlem1  25537  i1fd  25716  dvgt0lem2  26042  taylf  26402  efcvx  26493  logccv  26705  loglesqrt  26804  0elold  27947  noseqrdgfn  28312  usgredg2v  29244  crctcshtrl  29843  frgr3vlem1  30292  strlem6  32275  mptctf  32729  omsmeas  34325  sibfof  34342  bnj97  34880  bnj553  34912  bnj966  34958  bnj1442  35063  subfaclefac  35181  erdsze2lem1  35208  erdsze2lem2  35209  snmlff  35334  satffunlem2lem2  35411  bj-ssbid2ALT  36664  phpreu  37611  ptrecube  37627  poimirlem3  37630  poimirlem32  37659  heicant  37662  dvhopellsm  41119  aks5lem7  42201  pell1qrgaplem  42884  dnwech  43060  oaun3lem1  43387  mnurndlem1  44300  rn1st  45280  stoweid  46078  dirkercncflem2  46119  fourierdlem36  46158  usgrexmpl12ngric  47997  usgrexmpl12ngrlic  47998