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  5463  seqshft2  13963  seqsplit  13970  resqrex  15185  2mulprm  16632  comppfsc  23488  filconn  23839  sinq12ge0  26485  usgr2pth  29849  elwspths2on  30047  elwspths2onw  30048  frgr3vlem1  30360  3vfriswmgrlem  30364  onsupnmax  43582  cantnfresb  43678  dflim5  43683