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  3214  moeq3  3350  reusv1OLD  4793  fveqf1o  6457  fliftcnv  6461  fliftfun  6462  undom  7933  pwdom  7997  onomeneq  8035  pwfilem  8143  ordiso  8304  ordtypelem8  8313  wdompwdom  8366  unxpwdom  8377  harwdom  8378  infeq5i  8416  cantnfcl  8447  cardiun  8691  infxpenlem  8719  dfac8b  8737  acnnum  8758  inffien  8769  dfac12lem2  8849  cdadom3  8893  cdainflem  8896  cdainf  8897  infunabs  8912  infcda  8913  infdif  8914  infdif2  8915  infmap2  8923  fictb  8950  cofsmo  8974  fin23lem21  9044  hsmexlem1  9131  iundomg  9242  iunctb  9275  fpwwe2lem9  9339  canthnum  9350  winalim2  9397  rankcf  9478  tskuni  9484  npomex  9697  hashun2  13033  swrd2lsw  13543  2swrd2eqwrdeq  13544  limsupgord  14051  summolem2  14294  zsum  14296  prodmolem2  14504  zprod  14506  ltoddhalfle  14923  isinv  16243  invsym2  16246  invfun  16247  oppcsect2  16262  oppcinv  16263  efgcpbllemb  17991  frgpuplem  18008  gsumval3  18131  1stcfb  21058  1stcrestlem  21065  2ndcdisj2  21070  txdis1cn  21248  tx1stc  21263  tgphaus  21730  qustgplem  21734  tsmsxp  21768  xmeter  22048  bndth  22565  clmneg1  22690  ovolctb2  23067  ovoliunlem1  23077  i1fd  23254  dvgt0lem2  23570  taylf  23919  efcvx  24007  logccv  24209  loglesqrt  24299  usgraidx2v  25922  frgra3vlem1  26527  numclwlk1lem2f1  26621  strlem6  28499  dmct  28877  cnvct  28878  mptct  28880  mptctf  28883  omsmeas  29712  sibfof  29729  bnj97  30190  bnj553  30222  bnj966  30268  bnj1442  30371  subfaclefac  30412  erdsze2lem1  30439  erdsze2lem2  30440  snmlff  30565  orderseqlem  30993  frrlem5c  31030  bj-ssbid2ALT  31835  phpreu  32563  ptrecube  32579  poimirlem3  32582  poimirlem32  32611  heicant  32614  dvhopellsm  35424  pell1qrgaplem  36455  dnwech  36636  stoweid  38956  dirkercncflem2  38997  fourierdlem36  39036  usgredg2v  40454  crctcshtrl  41026  frgr3vlem1  41443  av-numclwlk1lem2f1  41524