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  2138  sbcrext  3810  oaordi  8353  nnaordi  8425  mapsnend  8796  cantnfval2  9388  infxpenc2lem1  9759  ackbij1lem16  9975  sornom  10017  fin23lem36  10088  isf32lem1  10093  isf32lem2  10094  zornn0g  10245  canthwe  10391  indpi  10647  seqid2  13750  pfxccatin12lem3  14426  fsum2d  15464  fsumabs  15494  fsumiun  15514  fprod2d  15672  prmodvdslcmf  16729  prmlem1a  16789  gicsubgen  18875  dmatelnd  21626  dis2ndc  22592  1stcelcls  22593  ptcmpfi  22945  caubl  24453  caublcls  24454  volsuplem  24700  cpnord  25080  fsumvma  26342  gausslemma2dlem4  26498  pntpbnd1  26715  3pthdlem1  28507  frgr3vlem1  28616  3vfriswmgrlem  28620  fzto1st  31349  psgnfzto1st  31351  wl-equsal1t  35679  ax12f  36933  incssnn0  40513  lzenom  40572  clsk1independent  41609  iidn3  42074  truniALT  42114  onfrALTlem2  42119  ee220  42211  dvmptfprodlem  43439  fourierdlem89  43690  fourierdlem91  43692  sge0reuz  43939  hoi2toco  44099  linds0  45758