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  3500  moeq3  3686  fvsng  7157  fveqf1o  7280  fliftcnv  7289  fliftfun  7290  frxp3  8133  orderseqlem  8139  cnvct  9008  undomOLD  9034  pwdom  9099  php  9177  ordiso  9476  ordtypelem8  9485  wdompwdom  9538  unxpwdom  9549  harwdom  9551  inf0  9581  infeq5i  9596  cantnfcl  9627  cardiun  9942  infxpenlem  9973  dfac8b  9991  acnnum  10012  inffien  10023  dfac12lem2  10105  djudoml  10145  cdainflem  10148  djuinf  10149  infunabs  10166  infdju  10167  infdif  10168  infdif2  10169  infmap2  10177  fictb  10204  cofsmo  10229  fin23lem21  10299  hsmexlem1  10386  dmct  10484  mptct  10498  iundomg  10501  iunctb  10534  fpwwe2lem8  10598  canthnum  10609  winalim2  10656  rankcf  10737  tskuni  10743  npomex  10956  hashun2  14355  swrd2lsw  14925  2swrd2eqwrdeq  14926  limsupgord  15445  summolem2  15689  zsum  15691  prodmolem2  15908  zprod  15910  ltoddhalfle  16338  isinv  17729  invsym2  17732  invfun  17733  oppcsect2  17748  oppcinv  17749  efgcpbllemb  19692  frgpuplem  19709  gsumval3  19844  1stcfb  23339  1stcrestlem  23346  2ndcdisj2  23351  txdis1cn  23529  tx1stc  23544  tgphaus  24011  qustgplem  24015  tsmsxp  24049  xmeter  24328  bndth  24864  clmneg1  24989  ovolctb2  25400  ovoliunlem1  25410  i1fd  25589  dvgt0lem2  25915  taylf  26275  efcvx  26366  logccv  26579  loglesqrt  26678  0elold  27828  noseqrdgfn  28207  n0sfincut  28253  usgredg2v  29161  crctcshtrl  29760  frgr3vlem1  30209  strlem6  32192  mptctf  32648  omsmeas  34321  sibfof  34338  bnj97  34863  bnj553  34895  bnj966  34941  bnj1442  35046  subfaclefac  35170  erdsze2lem1  35197  erdsze2lem2  35198  snmlff  35323  satffunlem2lem2  35400  bj-ssbid2ALT  36658  phpreu  37605  ptrecube  37621  poimirlem3  37624  poimirlem32  37653  heicant  37656  dvhopellsm  41118  aks5lem7  42195  pell1qrgaplem  42868  dnwech  43044  oaun3lem1  43370  mnurndlem1  44277  rn1st  45274  stoweid  46068  dirkercncflem2  46109  fourierdlem36  46148  usgrexmpl12ngric  48033  usgrexmpl12ngrlic  48034