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  14178  seqsplit  14185  resqrex  15426  2mulprm  16877  comppfsc  23860  filconn  24211  sinq12ge0  26846  usgr2pth  30359  elwspths2on  30560  elwspths2onw  30561  frgr3vlem1  30883  3vfriswmgrlem  30887  onsupnmax  44339  cantnfresb  44435  dflim5  44440  smprngprmrng  49544