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 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  propeqop  5488  seqshft2  14060  seqsplit  14067  resqrex  15297  2mulprm  16747  comppfsc  23654  filconn  24005  sinq12ge0  26635  usgr2pth  30050  elwspths2on  30248  elwspths2onw  30249  frgr3vlem1  30561  3vfriswmgrlem  30565  onsupnmax  43840  cantnfresb  43936  dflim5  43941  smprngprmrng  48986