Theorem syl9 77

Description: A nested syllogism inference with different antecedents. (Contributed by NM, 13-May-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.)

Hypotheses

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

Assertion

Ref	Expression
syl9	⊢ (𝜑 → (𝜃 → (𝜓 → 𝜏)))

Proof of Theorem syl9

Step	Hyp	Ref	Expression
1		syl9.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		syl9.2	. . 3 ⊢ (𝜃 → (𝜒 → 𝜏))
3	2	a1i 11	. 2 ⊢ (𝜑 → (𝜃 → (𝜒 → 𝜏)))
4	1, 3	syl5d 73	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:  syl9r  78  com23  86  sylan9  507  19.38a  1838  ax13lem1  2382  ax13lem2  2384  axc11n  2434  rspc6v  3656  reuss2  4345  reupick  4348  elinxp  6048  ordtr2  6439  suc11  6502  funimass4  6986  fliftfun  7348  omlimcl  8634  nneob  8712  rankwflemb  9862  cflm  10319  domtriomlem  10511  grothomex  10898  sup3  12252  caubnd  15407  fbflim2  24006  ellimc3  25934  usgruspgrb  29218  usgredgsscusgredg  29495  3cyclfrgrrn1  30317  dfon2lem6  35752  opnrebl2  36287  bj-nfimt  36604  axc11n11r  36649  bj-nnf-alrim  36721  stdpc5t  36793  wl-ax13lem1  37460  diaintclN  41015  dibintclN  41124  dihintcl  41301  sn-sup3d  42448  dflim5  43291  pm11.71  44366  axc11next  44375  rrx2plord2  48456