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  5455  seqshft2  13988  seqsplit  13995  resqrex  15210  2mulprm  16660  comppfsc  23522  filconn  23873  sinq12ge0  26497  usgr2pth  29857  elwspths2on  30055  elwspths2onw  30056  frgr3vlem1  30368  3vfriswmgrlem  30372  onsupnmax  43680  cantnfresb  43776  dflim5  43781