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  512  19.38a  1847  ax13lem1  2382  ax13lem2  2384  axc11n  2434  rspc6v  3581  reuss2  4254  reupick  4257  axprglem  5365  elinxp  5971  ordtr2  6355  suc11  6419  funimass4  6891  fliftfun  7256  omlimcl  8503  nneob  8582  rankwflemb  9708  cflm  10163  domtriomlem  10355  grothomex  10743  sup3  12104  caubnd  15312  fbflim2  23960  ellimc3  25864  usgruspgrb  29270  usgredgsscusgredg  29546  3cyclfrgrrn1  30373  dfon2lem6  36014  opnrebl2  36549  axtco1from2  36703  bj-nfimt  36963  axc11n11r  37026  bj-nnf-alrim  37088  stdpc5t  37180  wl-ax13lem1  37856  diaintclN  41550  dibintclN  41659  dihintcl  41836  sn-sup3d  42982  dflim5  43774  pm11.71  44841  axc11next  44850  rrx2plord2  49213