Theorem a1i13 28

Description: Add two antecedents to a wff. (Contributed by Jeff Hankins, 4-Aug-2009.)

Hypothesis

Ref	Expression
a1i13.1	⊢ (𝜓 → 𝜃)

Assertion

Ref	Expression
a1i13	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Proof of Theorem a1i13

Step	Hyp	Ref	Expression
1		a1i13.1	. . 3 ⊢ (𝜓 → 𝜃)
2	1	a1d 26	. 2 ⊢ (𝜓 → (𝜒 → 𝜃))
3	2	a1i 11	1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  propeqop  5492  seqshft2  14082  seqsplit  14089  resqrex  15325  2mulprm  16773  comppfsc  23740  filconn  24091  sinq12ge0  26724  usgr2pth  30177  elwspths2on  30378  elwspths2onw  30379  frgr3vlem1  30695  3vfriswmgrlem  30699  onsupnmax  44013  cantnfresb  44109  dflim5  44114  smprngprmrng  49161