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  1842  ax13lem1  2379  ax13lem2  2381  axc11n  2431  rspc6v  3599  reuss2  4280  reupick  4283  axprglem  5382  elinxp  5986  ordtr2  6370  suc11  6434  funimass4  6906  fliftfun  7268  omlimcl  8515  nneob  8594  rankwflemb  9717  cflm  10172  domtriomlem  10364  grothomex  10752  sup3  12111  caubnd  15294  fbflim2  23933  ellimc3  25848  usgruspgrb  29268  usgredgsscusgredg  29545  3cyclfrgrrn1  30372  dfon2lem6  36002  opnrebl2  36537  bj-nfimt  36874  axc11n11r  36928  bj-nnf-alrim  36988  stdpc5t  37075  wl-ax13lem1  37749  diaintclN  41434  dibintclN  41543  dihintcl  41720  sn-sup3d  42862  dflim5  43686  pm11.71  44753  axc11next  44762  rrx2plord2  49082