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  5486  seqshft2  14211  seqsplit  14218  resqrex  15460  2mulprm  16912  comppfsc  23906  filconn  24257  sinq12ge0  26894  usgr2pth  30407  elwspths2on  30608  elwspths2onw  30609  frgr3vlem1  30931  3vfriswmgrlem  30935  onsupnmax  44491  cantnfresb  44587  dflim5  44592  smprngprmrng  49767