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  2136  sbcrext  3868  mptexgf  7224  oaordi  8546  nnaordi  8618  mapsnend  9036  cantnfval2  9664  infxpenc2lem1  10014  ackbij1lem16  10230  sornom  10272  fin23lem36  10343  isf32lem1  10348  isf32lem2  10349  zornn0g  10500  canthwe  10646  indpi  10902  seqid2  14014  pfxccatin12lem3  14682  fsum2d  15717  fsumabs  15747  fsumiun  15767  fprod2d  15925  prmodvdslcmf  16980  prmlem1a  17040  gicsubgen  19152  dmatelnd  21998  dis2ndc  22964  1stcelcls  22965  ptcmpfi  23317  caubl  24825  caublcls  24826  volsuplem  25072  cpnord  25452  fsumvma  26716  gausslemma2dlem4  26872  pntpbnd1  27089  3pthdlem1  29417  frgr3vlem1  29526  3vfriswmgrlem  29530  fzto1st  32262  psgnfzto1st  32264  wl-equsal1t  36410  ax12f  37810  incssnn0  41449  lzenom  41508  omabs2  42082  clsk1independent  42797  iidn3  43262  truniALT  43302  onfrALTlem2  43307  ee220  43399  dvmptfprodlem  44660  fourierdlem89  44911  fourierdlem91  44913  sge0reuz  45163  hoi2toco  45323  linds0  47146