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 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  moeq3  3678  fvsng  7168  fveqf1o  7290  fliftcnv  7299  fliftfun  7300  frxp3  8135  orderseqlem  8141  cnvct  9019  pwdom  9105  php  9179  ordiso  9466  ordtypelem8  9475  wdompwdom  9528  unxpwdom  9539  harwdom  9541  inf0  9578  infeq5i  9593  cantnfcl  9624  cardiun  9956  infxpenlem  9985  dfac8b  10003  acnnum  10024  inffien  10035  dfac12lem2  10116  djudoml  10156  cdainflem  10159  djuinf  10160  infunabs  10177  infdju  10178  infdif  10179  infdif2  10180  infmap2  10188  fictb  10215  cofsmo  10241  fin23lem21  10311  hsmexlem1  10398  dmct  10496  mptct  10510  iundomg  10513  iunctb  10547  fpwwe2lem8  10611  canthnum  10622  winalim2  10669  rankcf  10750  tskuni  10756  npomex  10969  hashun2  14410  swrd2lsw  14979  2swrd2eqwrdeq  14980  limsupgord  15513  summolem2  15757  zsum  15759  prodmolem2  15979  zprod  15981  ltoddhalfle  16409  isinv  17807  invsym2  17810  invfun  17811  oppcsect2  17826  oppcinv  17827  efgcpbllemb  19816  frgpuplem  19833  gsumval3  19968  1stcfb  23563  1stcrestlem  23570  2ndcdisj2  23575  txdis1cn  23753  tx1stc  23768  tgphaus  24235  qustgplem  24239  tsmsxp  24273  xmeter  24551  bndth  25078  clmneg1  25202  ovolctb2  25612  ovoliunlem1  25622  i1fd  25801  dvgt0lem2  26123  taylf  26482  efcvx  26570  logccv  26786  loglesqrt  26884  0elold  28061  noseqrdgfn  28457  n0fincut  28506  usgredg2v  29486  crctcshtrl  30081  frgr3vlem1  30533  strlem6  32517  mptctf  32973  omsmeas  34630  sibfof  34647  bnj97  35171  bnj553  35203  bnj966  35249  bnj1442  35354  tz9.1regs  35442  subfaclefac  35539  erdsze2lem1  35566  erdsze2lem2  35567  snmlff  35692  satffunlem2lem2  35769  bj-ssbid2ALT  37147  phpreu  38115  ptrecube  38131  poimirlem3  38134  poimirlem32  38163  heicant  38166  dvhopellsm  41753  aks5lem7  42829  pell1qrgaplem  43462  dnwech  43637  oaun3lem1  43963  mnurndlem1  44855  rn1st  45846  stoweid  46635  dirkercncflem2  46676  fourierdlem36  46715  usgrexmpl12ngric  48658  usgrexmpl12ngrlic  48659