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  2077  sbcrext  3761  oaordi  7975  nnaordi  8047  mapsnend  8387  cantnfval2  8928  infxpenc2lem1  9241  ackbij1lem16  9457  sornom  9499  fin23lem36  9570  isf32lem1  9575  isf32lem2  9576  zornn0g  9727  canthwe  9873  indpi  10129  seqid2  13234  swrdccatin12lem3  13936  fsum2d  14989  fsumabs  15019  fsumiun  15039  fprod2d  15198  prmodvdslcmf  16242  prmlem1a  16299  gicsubgen  18192  dmatelnd  20812  dis2ndc  21775  1stcelcls  21776  ptcmpfi  22128  caubl  23617  caublcls  23618  volsuplem  23862  cpnord  24238  fsumvma  25494  gausslemma2dlem4  25650  pntpbnd1  25867  clwwlknonex2lem2  27639  3pthdlem1  27696  frgr3vlem1  27810  3vfriswmgrlem  27814  fzto1st  30694  psgnfzto1st  30696  wl-equsal1t  34223  ax12f  35521  incssnn0  38703  lzenom  38762  clsk1independent  39759  iidn3  40254  truniALT  40294  onfrALTlem2  40299  ee220  40391  dvmptfprodlem  41660  fourierdlem89  41912  fourierdlem91  41914  sge0reuz  42161  hoi2toco  42321  linds0  43888