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  638  pm2.36  793  pm4.72  812  const  837  pm2.18dc  840  con1dc  841  jadc  848  pm2.521dcALT  855  con1biimdc  858  condandc  866  pm5.18dc  868  pm2.68dc  879  annimdc  921  syl3an2  1250  syl2an23an  1277  xor3dc  1365  alrimdh  1455  spsd  1518  a5i  1522  19.21h  1536  hbnt  1631  hbae  1696  sbiedh  1760  exdistrfor  1772  sbcof2  1782  ax11a2  1793  ax11v  1799  sb4  1804  hbsb4t  1988  exmoeudc  2062  euimmo  2066  mopick  2077  r19.37  2583  spcimgft  2762  spcimegft  2764  rr19.28v  2824  mob2  2864  euind  2871  reuind  2889  sbeqalb  2965  triun  4039  csbexga  4056  copsexg  4166  trssord  4302  trsuc  4344  trsucss  4345  abnexg  4367  ralxfrd  4383  rexxfrd  4384  ralxfrALT  4388  sucprcreg  4464  nlimsucg  4481  tfis  4497  relssres  4857  issref  4921  dmsnopg  5010  dfco2a  5039  imadif  5203  fvelima  5473  mptfvex  5506  fvmptdf  5508  fvmptf  5513  funfvima2  5650  funfvima3  5651  foco2  5655  isores3  5716  oprabid  5803  ovmpt4g  5893  ovmpos  5894  ov2gf  5895  ovmpodf  5902  suppssfv  5978  suppssov1  5979  fo2ndf  6124  rntpos  6154  tposf2  6165  nnmordi  6412  nnmord  6413  nnaordex  6423  ectocld  6495  qsel  6506  mapsn  6584  f1oeng  6651  mapen  6740  nneneq  6751  findcard2  6783  findcard2s  6784  ac6sfi  6792  fiintim  6817  sbthlem1  6845  pr2ne  7048  ltbtwnnqq  7223  prnmaddl  7298  genpcdl  7327  genpcuu  7328  ltaddpr  7405  lteupri  7425  recexprlemss1l  7443  recexprlemss1u  7444  cauappcvgprlemdisj  7459  lttrsr  7570  recexgt0sr  7581  mulgt0sr  7586  axprecex  7688  rereceu  7697  addlsub  8132  recexap  8414  0mnnnnn0  9009  prime  9150  zeo  9156  fnn0ind  9167  zindd  9169  btwnz  9170  lbzbi  9408  addmodlteq  10171  facwordi  10486  seq3coll  10585  qdenre  10974  climcau  11116  serf0  11121  zsumdc  11153  fsum2dlemstep  11203  fsum2d  11204  fsumabs  11234  fsumiun  11246  odd2np1  11570  ndvdssub  11627  dfgcd2  11702  nprm  11804  rpexp  11831  lmss  12415  lmtopcnp  12419  txcn  12444  txlm  12448  xmettri2  12530  blin2  12601  metcnp3  12680  limcresi  12804  bj-stim  12954  bj-stan  12955  bj-stand  12956  bj-stal  12957  bj-sbimedh  12978  bj-vtoclgft  12982  elabgft1  12985  elabgf2  12987