Theorem a1i13 27

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 25	. 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  5461  seqshft2  13990  seqsplit  13997  resqrex  15212  2mulprm  16662  comppfsc  23497  filconn  23848  sinq12ge0  26472  usgr2pth  29832  elwspths2on  30030  elwspths2onw  30031  frgr3vlem1  30343  3vfriswmgrlem  30347  onsupnmax  43656  cantnfresb  43752  dflim5  43757