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  5452  seqshft2  13942  seqsplit  13949  resqrex  15164  2mulprm  16611  comppfsc  23467  filconn  23818  sinq12ge0  26464  usgr2pth  29763  elwspths2on  29961  elwspths2onw  29962  frgr3vlem1  30274  3vfriswmgrlem  30278  onsupnmax  43385  cantnfresb  43481  dflim5  43486