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  2144  sbcrext  3820  mptexgf  7162  oaordi  8467  nnaordi  8539  mapsnend  8965  cantnfval2  9566  infxpenc2lem1  9917  ackbij1lem16  10132  sornom  10175  fin23lem36  10246  isf32lem1  10251  isf32lem2  10252  zornn0g  10403  canthwe  10549  indpi  10805  seqid2  13957  pfxccatin12lem3  14641  fsum2d  15680  fsumabs  15710  fsumiun  15730  fprod2d  15890  prmodvdslcmf  16961  prmlem1a  17020  gicsubgen  19193  dmatelnd  22412  dis2ndc  23376  1stcelcls  23377  ptcmpfi  23729  caubl  25236  caublcls  25237  volsuplem  25484  cpnord  25865  fsumvma  27152  gausslemma2dlem4  27308  pntpbnd1  27525  3pthdlem1  30146  frgr3vlem1  30255  3vfriswmgrlem  30259  fzto1st  33079  psgnfzto1st  33081  wl-equsal1t  37607  ax12f  39059  incssnn0  42828  lzenom  42887  omabs2  43449  clsk1independent  44163  iidn3  44618  truniALT  44658  onfrALTlem2  44663  ee220  44755  dvmptfprodlem  46066  dvnprodlem1  46068  fourierdlem89  46317  fourierdlem91  46319  sge0reuz  46569  hoi2toco  46729  gpgedg2iv  48191  linds0  48590