Theorem 2a1i 12

Description: Inference introducing two antecedents. Two applications of a1i 11. Inference associated with 2a1 28. (Contributed by Jeff Hankins, 4-Aug-2009.)

Hypothesis

Ref	Expression
2a1i.1	⊢ 𝜑

Assertion

Ref	Expression
2a1i	⊢ (𝜓 → (𝜒 → 𝜑))

Proof of Theorem 2a1i

Step	Hyp	Ref	Expression
1		2a1i.1	. . 3 ⊢ 𝜑
2	1	a1i 11	. 2 ⊢ (𝜒 → 𝜑)
3	2	a1i 11	1 ⊢ (𝜓 → (𝜒 → 𝜑))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6

This theorem is referenced by:  ax13dgen3  2144  sbcrext  3823  mptexgf  7168  oaordi  8473  nnaordi  8546  mapsnend  8973  cantnfval2  9578  infxpenc2lem1  9929  ackbij1lem16  10144  sornom  10187  fin23lem36  10258  isf32lem1  10263  isf32lem2  10264  zornn0g  10415  canthwe  10562  indpi  10818  seqid2  13971  pfxccatin12lem3  14655  fsum2d  15694  fsumabs  15724  fsumiun  15744  fprod2d  15904  prmodvdslcmf  16975  prmlem1a  17034  gicsubgen  19208  dmatelnd  22440  dis2ndc  23404  1stcelcls  23405  ptcmpfi  23757  caubl  25264  caublcls  25265  volsuplem  25512  cpnord  25893  fsumvma  27180  gausslemma2dlem4  27336  pntpbnd1  27553  3pthdlem1  30239  frgr3vlem1  30348  3vfriswmgrlem  30352  fzto1st  33185  psgnfzto1st  33187  wl-equsal1t  37743  ax12f  39196  incssnn0  42949  lzenom  43008  omabs2  43570  clsk1independent  44283  iidn3  44738  truniALT  44778  onfrALTlem2  44783  ee220  44875  dvmptfprodlem  46184  dvnprodlem1  46186  fourierdlem89  46435  fourierdlem91  46437  sge0reuz  46687  hoi2toco  46847  gpgedg2iv  48309  linds0  48707