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  3846  mptexgf  7211  oaordi  8553  nnaordi  8625  mapsnend  9045  cantnfval2  9676  infxpenc2lem1  10026  ackbij1lem16  10241  sornom  10284  fin23lem36  10355  isf32lem1  10360  isf32lem2  10361  zornn0g  10512  canthwe  10658  indpi  10914  seqid2  14056  pfxccatin12lem3  14739  fsum2d  15776  fsumabs  15806  fsumiun  15826  fprod2d  15986  prmodvdslcmf  17054  prmlem1a  17113  gicsubgen  19249  dmatelnd  22421  dis2ndc  23385  1stcelcls  23386  ptcmpfi  23738  caubl  25247  caublcls  25248  volsuplem  25495  cpnord  25876  fsumvma  27162  gausslemma2dlem4  27318  pntpbnd1  27535  3pthdlem1  30079  frgr3vlem1  30188  3vfriswmgrlem  30192  fzto1st  33051  psgnfzto1st  33053  wl-equsal1t  37489  ax12f  38887  incssnn0  42666  lzenom  42725  omabs2  43288  clsk1independent  44002  iidn3  44459  truniALT  44499  onfrALTlem2  44504  ee220  44596  dvmptfprodlem  45909  dvnprodlem1  45911  fourierdlem89  46160  fourierdlem91  46162  sge0reuz  46412  hoi2toco  46572  linds0  48335