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  2139  sbcrext  3811  oaordi  8369  nnaordi  8441  mapsnend  8818  cantnfval2  9415  infxpenc2lem1  9786  ackbij1lem16  10002  sornom  10044  fin23lem36  10115  isf32lem1  10120  isf32lem2  10121  zornn0g  10272  canthwe  10418  indpi  10674  seqid2  13780  pfxccatin12lem3  14456  fsum2d  15494  fsumabs  15524  fsumiun  15544  fprod2d  15702  prmodvdslcmf  16759  prmlem1a  16819  gicsubgen  18905  dmatelnd  21656  dis2ndc  22622  1stcelcls  22623  ptcmpfi  22975  caubl  24483  caublcls  24484  volsuplem  24730  cpnord  25110  fsumvma  26372  gausslemma2dlem4  26528  pntpbnd1  26745  3pthdlem1  28537  frgr3vlem1  28646  3vfriswmgrlem  28650  fzto1st  31379  psgnfzto1st  31381  wl-equsal1t  35709  ax12f  36963  incssnn0  40542  lzenom  40601  clsk1independent  41638  iidn3  42103  truniALT  42143  onfrALTlem2  42148  ee220  42240  dvmptfprodlem  43467  fourierdlem89  43718  fourierdlem91  43720  sge0reuz  43967  hoi2toco  44127  linds0  45785