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  2139  sbcrext  3848  mptexgf  7214  oaordi  8558  nnaordi  8630  mapsnend  9050  cantnfval2  9683  infxpenc2lem1  10033  ackbij1lem16  10248  sornom  10291  fin23lem36  10362  isf32lem1  10367  isf32lem2  10368  zornn0g  10519  canthwe  10665  indpi  10921  seqid2  14066  pfxccatin12lem3  14750  fsum2d  15787  fsumabs  15817  fsumiun  15837  fprod2d  15997  prmodvdslcmf  17067  prmlem1a  17126  gicsubgen  19262  dmatelnd  22434  dis2ndc  23398  1stcelcls  23399  ptcmpfi  23751  caubl  25260  caublcls  25261  volsuplem  25508  cpnord  25889  fsumvma  27176  gausslemma2dlem4  27332  pntpbnd1  27549  3pthdlem1  30145  frgr3vlem1  30254  3vfriswmgrlem  30258  fzto1st  33114  psgnfzto1st  33116  wl-equsal1t  37560  ax12f  38958  incssnn0  42734  lzenom  42793  omabs2  43356  clsk1independent  44070  iidn3  44526  truniALT  44566  onfrALTlem2  44571  ee220  44663  dvmptfprodlem  45973  dvnprodlem1  45975  fourierdlem89  46224  fourierdlem91  46226  sge0reuz  46476  hoi2toco  46636  linds0  48441