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  5479  seqshft2  14164  seqsplit  14171  resqrex  15410  2mulprm  16861  comppfsc  23844  filconn  24195  sinq12ge0  26830  usgr2pth  30343  elwspths2on  30544  elwspths2onw  30545  frgr3vlem1  30867  3vfriswmgrlem  30871  onsupnmax  44214  cantnfresb  44310  dflim5  44315  smprngprmrng  49405