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  3873  mptexgf  7242  oaordi  8584  nnaordi  8656  mapsnend  9076  cantnfval2  9709  infxpenc2lem1  10059  ackbij1lem16  10274  sornom  10317  fin23lem36  10388  isf32lem1  10393  isf32lem2  10394  zornn0g  10545  canthwe  10691  indpi  10947  seqid2  14089  pfxccatin12lem3  14770  fsum2d  15807  fsumabs  15837  fsumiun  15857  fprod2d  16017  prmodvdslcmf  17085  prmlem1a  17144  gicsubgen  19297  dmatelnd  22502  dis2ndc  23468  1stcelcls  23469  ptcmpfi  23821  caubl  25342  caublcls  25343  volsuplem  25590  cpnord  25971  fsumvma  27257  gausslemma2dlem4  27413  pntpbnd1  27630  3pthdlem1  30183  frgr3vlem1  30292  3vfriswmgrlem  30296  fzto1st  33123  psgnfzto1st  33125  wl-equsal1t  37543  ax12f  38941  incssnn0  42722  lzenom  42781  omabs2  43345  clsk1independent  44059  iidn3  44521  truniALT  44561  onfrALTlem2  44566  ee220  44658  dvmptfprodlem  45959  dvnprodlem1  45961  fourierdlem89  46210  fourierdlem91  46212  sge0reuz  46462  hoi2toco  46622  linds0  48382