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:  moeq3  3674  fvsng  7160  fveqf1o  7282  fliftcnv  7291  fliftfun  7292  frxp3  8126  orderseqlem  8132  cnvct  9011  pwdom  9097  php  9171  ordiso  9461  ordtypelem8  9470  wdompwdom  9523  unxpwdom  9534  harwdom  9536  inf0  9573  infeq5i  9588  cantnfcl  9619  cardiun  9937  infxpenlem  9966  dfac8b  9984  acnnum  10005  inffien  10016  dfac12lem2  10098  djudoml  10138  cdainflem  10141  djuinf  10142  infunabs  10159  infdju  10160  infdif  10161  infdif2  10162  infmap2  10170  fictb  10197  cofsmo  10223  fin23lem21  10293  hsmexlem1  10380  dmct  10478  mptct  10492  iundomg  10495  iunctb  10529  fpwwe2lem8  10593  canthnum  10604  winalim2  10651  rankcf  10732  tskuni  10738  npomex  10951  hashun2  14393  swrd2lsw  14962  2swrd2eqwrdeq  14963  limsupgord  15482  summolem2  15726  zsum  15728  prodmolem2  15948  zprod  15950  ltoddhalfle  16378  isinv  17776  invsym2  17779  invfun  17780  oppcsect2  17795  oppcinv  17796  efgcpbllemb  19778  frgpuplem  19795  gsumval3  19930  1stcfb  23485  1stcrestlem  23492  2ndcdisj2  23497  txdis1cn  23675  tx1stc  23690  tgphaus  24157  qustgplem  24161  tsmsxp  24195  xmeter  24473  bndth  25000  clmneg1  25124  ovolctb2  25534  ovoliunlem1  25544  i1fd  25723  dvgt0lem2  26045  taylf  26401  efcvx  26489  logccv  26705  loglesqrt  26803  0elold  27980  noseqrdgfn  28376  n0fincut  28425  usgredg2v  29374  crctcshtrl  29969  frgr3vlem1  30421  strlem6  32405  mptctf  32868  omsmeas  34581  sibfof  34598  bnj97  35125  bnj553  35157  bnj966  35203  bnj1442  35308  tz9.1regs  35394  subfaclefac  35490  erdsze2lem1  35517  erdsze2lem2  35518  snmlff  35643  satffunlem2lem2  35720  bj-ssbid2ALT  37099  phpreu  38067  ptrecube  38083  poimirlem3  38086  poimirlem32  38115  heicant  38118  dvhopellsm  41705  aks5lem7  42781  pell1qrgaplem  43414  dnwech  43589  oaun3lem1  43915  mnurndlem1  44821  rn1st  45812  stoweid  46601  dirkercncflem2  46642  fourierdlem36  46681  usgrexmpl12ngric  48624  usgrexmpl12ngrlic  48625