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  2135  sbcrext  3867  mptexgf  7223  oaordi  8545  nnaordi  8617  mapsnend  9035  cantnfval2  9663  infxpenc2lem1  10013  ackbij1lem16  10229  sornom  10271  fin23lem36  10342  isf32lem1  10347  isf32lem2  10348  zornn0g  10499  canthwe  10645  indpi  10901  seqid2  14013  pfxccatin12lem3  14681  fsum2d  15716  fsumabs  15746  fsumiun  15766  fprod2d  15924  prmodvdslcmf  16979  prmlem1a  17039  gicsubgen  19151  dmatelnd  21997  dis2ndc  22963  1stcelcls  22964  ptcmpfi  23316  caubl  24824  caublcls  24825  volsuplem  25071  cpnord  25451  fsumvma  26713  gausslemma2dlem4  26869  pntpbnd1  27086  3pthdlem1  29414  frgr3vlem1  29523  3vfriswmgrlem  29527  fzto1st  32257  psgnfzto1st  32259  wl-equsal1t  36405  ax12f  37805  incssnn0  41439  lzenom  41498  omabs2  42072  clsk1independent  42787  iidn3  43252  truniALT  43292  onfrALTlem2  43297  ee220  43389  dvmptfprodlem  44650  fourierdlem89  44901  fourierdlem91  44903  sge0reuz  45153  hoi2toco  45313  linds0  47136