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  3486  moeq3  3671  fvsng  7114  fveqf1o  7236  fliftcnv  7245  fliftfun  7246  frxp3  8081  orderseqlem  8087  cnvct  8956  pwdom  9042  php  9116  ordiso  9402  ordtypelem8  9411  wdompwdom  9464  unxpwdom  9475  harwdom  9477  inf0  9511  infeq5i  9526  cantnfcl  9557  cardiun  9872  infxpenlem  9901  dfac8b  9919  acnnum  9940  inffien  9951  dfac12lem2  10033  djudoml  10073  cdainflem  10076  djuinf  10077  infunabs  10094  infdju  10095  infdif  10096  infdif2  10097  infmap2  10105  fictb  10132  cofsmo  10157  fin23lem21  10227  hsmexlem1  10314  dmct  10412  mptct  10426  iundomg  10429  iunctb  10462  fpwwe2lem8  10526  canthnum  10537  winalim2  10584  rankcf  10665  tskuni  10671  npomex  10884  hashun2  14287  swrd2lsw  14856  2swrd2eqwrdeq  14857  limsupgord  15376  summolem2  15620  zsum  15622  prodmolem2  15839  zprod  15841  ltoddhalfle  16269  isinv  17664  invsym2  17667  invfun  17668  oppcsect2  17683  oppcinv  17684  efgcpbllemb  19665  frgpuplem  19682  gsumval3  19817  1stcfb  23358  1stcrestlem  23365  2ndcdisj2  23370  txdis1cn  23548  tx1stc  23563  tgphaus  24030  qustgplem  24034  tsmsxp  24068  xmeter  24346  bndth  24882  clmneg1  25007  ovolctb2  25418  ovoliunlem1  25428  i1fd  25607  dvgt0lem2  25933  taylf  26293  efcvx  26384  logccv  26597  loglesqrt  26696  0elold  27853  noseqrdgfn  28234  n0sfincut  28280  usgredg2v  29203  crctcshtrl  29799  frgr3vlem1  30248  strlem6  32231  mptctf  32694  omsmeas  34331  sibfof  34348  bnj97  34873  bnj553  34905  bnj966  34951  bnj1442  35056  tz9.1regs  35118  subfaclefac  35208  erdsze2lem1  35235  erdsze2lem2  35236  snmlff  35361  satffunlem2lem2  35438  bj-ssbid2ALT  36696  phpreu  37643  ptrecube  37659  poimirlem3  37662  poimirlem32  37691  heicant  37694  dvhopellsm  41155  aks5lem7  42232  pell1qrgaplem  42905  dnwech  43080  oaun3lem1  43406  mnurndlem1  44313  rn1st  45309  stoweid  46100  dirkercncflem2  46141  fourierdlem36  46180  usgrexmpl12ngric  48068  usgrexmpl12ngrlic  48069