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  5492  seqshft2  14066  seqsplit  14073  resqrex  15303  2mulprm  16752  comppfsc  23670  filconn  24021  sinq12ge0  26654  usgr2pth  30094  elwspths2on  30292  elwspths2onw  30293  frgr3vlem1  30605  3vfriswmgrlem  30609  onsupnmax  43938  cantnfresb  44034  dflim5  44039  smprngprmrng  49087