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  2003  sbcrext  3478  sbcrextOLD  3479  oaordi  7513  nnaordi  7585  map1  7921  cantnfval2  8449  infxpenc2lem1  8725  ackbij1lem16  8940  sornom  8982  fin23lem36  9053  isf32lem1  9058  isf32lem2  9059  zornn0g  9210  canthwe  9352  indpi  9608  seqid2  12709  swrdccatin12lem3  13341  fsum2d  14344  fsumabs  14374  fsumiun  14394  fprod2d  14550  prmodvdslcmf  15589  prmlem1a  15651  gicsubgen  17544  dmatelnd  20121  dis2ndc  21073  1stcelcls  21074  ptcmpfi  21426  caubl  22914  caublcls  22915  volsuplem  23130  cpnord  23504  fsumvma  24738  gausslemma2dlem4  24894  pntpbnd1  25075  frgra3vlem1  26527  3vfriswmgralem  26531  fzto1st  29184  psgnfzto1st  29186  bj-xnex  32245  wl-equsal1t  32506  ax12f  33243  incssnn0  36292  lzenom  36351  clsk1independent  37364  iidn3  37728  truniALT  37772  onfrALTlem2  37782  ee220  37884  dvmptfprodlem  38834  fourierdlem89  39088  fourierdlem91  39090  sge0reuz  39340  hoi2toco  39497  3pthdlem1  41331  frgr3vlem1  41443  3vfriswmgrlem  41447  linds0  42048