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  2145  sbcrext  3811  mptexgf  7177  oaordi  8481  nnaordi  8554  mapsnend  8983  cantnfval2  9590  infxpenc2lem1  9941  ackbij1lem16  10156  sornom  10199  fin23lem36  10270  isf32lem1  10275  isf32lem2  10276  zornn0g  10427  canthwe  10574  indpi  10830  seqid2  14010  pfxccatin12lem3  14694  fsum2d  15733  fsumabs  15764  fsumiun  15784  fprod2d  15946  prmodvdslcmf  17018  prmlem1a  17077  gicsubgen  19254  dmatelnd  22461  dis2ndc  23425  1stcelcls  23426  ptcmpfi  23778  caubl  25275  caublcls  25276  volsuplem  25522  cpnord  25902  fsumvma  27176  gausslemma2dlem4  27332  pntpbnd1  27549  3pthdlem1  30234  frgr3vlem1  30343  3vfriswmgrlem  30347  fzto1st  33164  psgnfzto1st  33166  wl-equsal1t  37867  disjimeceqbi2  39128  ax12f  39386  incssnn0  43143  lzenom  43202  omabs2  43760  clsk1independent  44473  iidn3  44928  truniALT  44968  onfrALTlem2  44973  ee220  45065  dvmptfprodlem  46372  dvnprodlem1  46374  fourierdlem89  46623  fourierdlem91  46625  sge0reuz  46875  hoi2toco  47035  gpgedg2iv  48543  linds0  48941