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  5484  seqshft2  14092  seqsplit  14099  resqrex  15337  2mulprm  16783  comppfsc  23758  filconn  24109  sinq12ge0  26746  usgr2pth  30229  elwspths2on  30430  elwspths2onw  30431  frgr3vlem1  30753  3vfriswmgrlem  30757  onsupnmax  44069  cantnfresb  44165  dflim5  44170  smprngprmrng  49254