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  13981  seqsplit  13988  resqrex  15203  2mulprm  16653  comppfsc  23507  filconn  23858  sinq12ge0  26485  usgr2pth  29847  elwspths2on  30045  elwspths2onw  30046  frgr3vlem1  30358  3vfriswmgrlem  30362  onsupnmax  43674  cantnfresb  43770  dflim5  43775