Theorem syl5 32

Description: A syllogism rule of inference. The second premise is used to replace the second antecedent of the first premise. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 25-May-2013.)

Hypotheses

Ref	Expression
syl5.1	⊢ (𝜑 → 𝜓)
syl5.2	⊢ (𝜒 → (𝜓 → 𝜃))

Assertion

Ref	Expression
syl5	⊢ (𝜒 → (𝜑 → 𝜃))

Proof of Theorem syl5

Step	Hyp	Ref	Expression
1		syl5.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl5.2	. . 3 ⊢ (𝜒 → (𝜓 → 𝜃))
3	1, 2	syl5com 29	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	3	com12 30	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:  syl56  34  syl2im  38  imim12i  59  pm2.86d  99  syl5bi  151  syl5bir  152  syl5ib  153  adantld  276  adantrd  277  impel  278  mpan9  279  nsyli  644  pm2.36  799  pm4.72  822  pm2.18dc  850  con1dc  851  jadc  858  pm2.521dcALT  865  con1biimdc  868  condandc  876  pm5.18dc  878  pm2.68dc  889  annimdc  932  syl3an2  1267  syl2an23an  1294  xor3dc  1382  alrimdh  1472  spsd  1531  a5i  1536  19.21h  1550  hbnt  1646  hbae  1711  sbiedh  1780  exdistrfor  1793  sbcof2  1803  ax11a2  1814  ax11v  1820  sb4  1825  hbsb4t  2006  exmoeudc  2082  euimmo  2086  mopick  2097  r19.37  2622  spcimgft  2806  spcimegft  2808  rr19.28v  2870  mob2  2910  euind  2917  reuind  2935  sbeqalb  3011  triun  4098  csbexga  4115  copsexg  4227  trssord  4363  trsuc  4405  trsucss  4406  abnexg  4429  ralxfrd  4445  rexxfrd  4446  ralxfrALT  4450  sucprcreg  4531  nlimsucg  4548  tfis  4565  relssres  4927  issref  4991  dmsnopg  5080  dfco2a  5109  imadif  5276  fvelima  5546  mptfvex  5579  fvmptdf  5581  fvmptf  5586  funfvima2  5725  funfvima3  5726  foco2  5730  isores3  5791  oprabid  5882  ovmpt4g  5972  ovmpos  5973  ov2gf  5974  ovmpodf  5981  suppssfv  6054  suppssov1  6055  fo2ndf  6203  rntpos  6233  tposf2  6244  nnmordi  6492  nnmord  6493  nnaordex  6503  ectocld  6575  qsel  6586  mapsn  6664  f1oeng  6731  mapen  6820  nneneq  6831  findcard2  6863  findcard2s  6864  ac6sfi  6872  fiintim  6902  sbthlem1  6930  pr2ne  7156  ltbtwnnqq  7364  prnmaddl  7439  genpcdl  7468  genpcuu  7469  ltaddpr  7546  lteupri  7566  recexprlemss1l  7584  recexprlemss1u  7585  cauappcvgprlemdisj  7600  lttrsr  7711  recexgt0sr  7722  mulgt0sr  7727  axprecex  7829  rereceu  7838  addlsub  8276  recexap  8558  0mnnnnn0  9154  prime  9298  zeo  9304  fnn0ind  9315  zindd  9317  btwnz  9318  lbzbi  9562  addmodlteq  10341  facwordi  10661  seq3coll  10764  qdenre  11153  climcau  11297  serf0  11302  zsumdc  11334  fsum2dlemstep  11384  fsum2d  11385  fsumabs  11415  fsumiun  11427  zproddc  11529  fprod2dlemstep  11572  fprod2d  11573  odd2np1  11819  ndvdssub  11876  dfgcd2  11956  nprm  12064  rpexp  12094  pc2dvds  12270  pcfac  12289  lmss  12961  lmtopcnp  12965  txcn  12990  txlm  12994  xmettri2  13076  blin2  13147  metcnp3  13226  limcresi  13350  logbgcd1irr  13600  lgsdir2lem2  13645  lgsne0  13654  2sqlem6  13671  2sqlem10  13676  bj-stim  13702  bj-stan  13703  bj-stand  13704  bj-stal  13705  bj-sbimedh  13727  bj-vtoclgft  13731  elabgft1  13734  elabgf2  13736