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  2150  sbcrext  3812  mptexgf  7173  oaordi  8478  nnaordi  8551  mapsnend  8980  cantnfval2  9588  infxpenc2lem1  9939  ackbij1lem16  10154  sornom  10197  fin23lem36  10268  isf32lem1  10273  isf32lem2  10274  zornn0g  10425  canthwe  10572  indpi  10828  seqid2  14008  pfxccatin12lem3  14692  fsum2d  15731  fsumabs  15762  fsumiun  15782  fprod2d  15944  prmodvdslcmf  17016  prmlem1a  17075  gicsubgen  19252  dmatelnd  22486  dis2ndc  23450  1stcelcls  23451  ptcmpfi  23803  caubl  25300  caublcls  25301  volsuplem  25547  cpnord  25927  fsumvma  27201  gausslemma2dlem4  27357  pntpbnd1  27574  3pthdlem1  30259  frgr3vlem1  30368  3vfriswmgrlem  30372  fzto1st  33191  psgnfzto1st  33193  wl-equsal1t  37920  disjimeceqbi2  39181  ax12f  39439  incssnn0  43167  lzenom  43226  omabs2  43784  clsk1independent  44497  iidn3  44952  truniALT  44992  onfrALTlem2  44997  ee220  45089  dvmptfprodlem  46394  dvnprodlem1  46396  fourierdlem89  46645  fourierdlem91  46647  sge0reuz  46897  hoi2toco  47057  gpgedg2iv  48565  linds0  48963