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  2141  sbcrext  3772  oaordi  8252  nnaordi  8324  mapsnend  8691  cantnfval2  9262  infxpenc2lem1  9598  ackbij1lem16  9814  sornom  9856  fin23lem36  9927  isf32lem1  9932  isf32lem2  9933  zornn0g  10084  canthwe  10230  indpi  10486  seqid2  13587  pfxccatin12lem3  14262  fsum2d  15298  fsumabs  15328  fsumiun  15348  fprod2d  15506  prmodvdslcmf  16563  prmlem1a  16623  gicsubgen  18636  dmatelnd  21347  dis2ndc  22311  1stcelcls  22312  ptcmpfi  22664  caubl  24159  caublcls  24160  volsuplem  24406  cpnord  24786  fsumvma  26048  gausslemma2dlem4  26204  pntpbnd1  26421  3pthdlem1  28201  frgr3vlem1  28310  3vfriswmgrlem  28314  fzto1st  31043  psgnfzto1st  31045  wl-equsal1t  35386  ax12f  36640  incssnn0  40177  lzenom  40236  clsk1independent  41274  iidn3  41735  truniALT  41775  onfrALTlem2  41780  ee220  41872  dvmptfprodlem  43103  fourierdlem89  43354  fourierdlem91  43356  sge0reuz  43603  hoi2toco  43763  linds0  45422