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  2142  sbcrext  3824  mptexgf  7156  oaordi  8461  nnaordi  8533  mapsnend  8958  cantnfval2  9559  infxpenc2lem1  9907  ackbij1lem16  10122  sornom  10165  fin23lem36  10236  isf32lem1  10241  isf32lem2  10242  zornn0g  10393  canthwe  10539  indpi  10795  seqid2  13952  pfxccatin12lem3  14636  fsum2d  15675  fsumabs  15705  fsumiun  15725  fprod2d  15885  prmodvdslcmf  16956  prmlem1a  17015  gicsubgen  19189  dmatelnd  22409  dis2ndc  23373  1stcelcls  23374  ptcmpfi  23726  caubl  25233  caublcls  25234  volsuplem  25481  cpnord  25862  fsumvma  27149  gausslemma2dlem4  27305  pntpbnd1  27522  3pthdlem1  30139  frgr3vlem1  30248  3vfriswmgrlem  30252  fzto1st  33067  psgnfzto1st  33069  wl-equsal1t  37575  ax12f  38978  incssnn0  42743  lzenom  42802  omabs2  43364  clsk1independent  44078  iidn3  44533  truniALT  44573  onfrALTlem2  44578  ee220  44670  dvmptfprodlem  45981  dvnprodlem1  45983  fourierdlem89  46232  fourierdlem91  46234  sge0reuz  46484  hoi2toco  46644  gpgedg2iv  48097  linds0  48496