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:  ceqsex  3434  moeq3  3578  fveqf1o  6778  fliftcnv  6782  fliftfun  6783  cnvct  8266  undom  8284  pwdom  8348  onomeneq  8386  pwfilem  8496  ordiso  8657  ordtypelem8  8666  wdompwdom  8719  unxpwdom  8730  harwdom  8731  infeq5i  8777  cantnfcl  8808  cardiun  9088  infxpenlem  9116  dfac8b  9134  acnnum  9155  inffien  9166  dfac12lem2  9248  cdadom3  9292  cdainflem  9295  cdainf  9296  infunabs  9311  infcda  9312  infdif  9313  infdif2  9314  infmap2  9322  fictb  9349  cofsmo  9373  fin23lem21  9443  hsmexlem1  9530  dmct  9628  mptct  9642  iundomg  9645  iunctb  9678  fpwwe2lem9  9742  canthnum  9753  winalim2  9800  rankcf  9881  tskuni  9887  npomex  10100  hashun2  13386  swrd2lsw  13916  2swrd2eqwrdeq  13917  limsupgord  14422  summolem2  14666  zsum  14668  prodmolem2  14882  zprod  14884  ltoddhalfle  15301  isinv  16620  invsym2  16623  invfun  16624  oppcsect2  16639  oppcinv  16640  efgcpbllemb  18365  frgpuplem  18382  gsumval3  18505  1stcfb  21458  1stcrestlem  21465  2ndcdisj2  21470  txdis1cn  21648  tx1stc  21663  tgphaus  22129  qustgplem  22133  tsmsxp  22167  xmeter  22447  bndth  22966  clmneg1  23090  ovolctb2  23469  ovoliunlem1  23479  i1fd  23658  dvgt0lem2  23976  taylf  24325  efcvx  24413  logccv  24619  loglesqrt  24709  usgredg2v  26330  crctcshtrl  26940  frgr3vlem1  27444  strlem6  29440  mptctf  29819  omsmeas  30707  sibfof  30724  bnj97  31256  bnj553  31288  bnj966  31334  bnj1442  31437  subfaclefac  31478  erdsze2lem1  31505  erdsze2lem2  31506  snmlff  31631  orderseqlem  32070  frrlem5c  32104  bj-ssbid2ALT  32958  phpreu  33703  ptrecube  33719  poimirlem3  33722  poimirlem32  33751  heicant  33754  dvhopellsm  36895  pell1qrgaplem  37936  dnwech  38116  stoweid  40756  dirkercncflem2  40797  fourierdlem36  40836