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  2133  sbcrext  3811  mptexgf  7130  oaordi  8408  nnaordi  8480  mapsnend  8861  cantnfval2  9471  infxpenc2lem1  9821  ackbij1lem16  10037  sornom  10079  fin23lem36  10150  isf32lem1  10155  isf32lem2  10156  zornn0g  10307  canthwe  10453  indpi  10709  seqid2  13815  pfxccatin12lem3  14490  fsum2d  15528  fsumabs  15558  fsumiun  15578  fprod2d  15736  prmodvdslcmf  16793  prmlem1a  16853  gicsubgen  18939  dmatelnd  21690  dis2ndc  22656  1stcelcls  22657  ptcmpfi  23009  caubl  24517  caublcls  24518  volsuplem  24764  cpnord  25144  fsumvma  26406  gausslemma2dlem4  26562  pntpbnd1  26779  3pthdlem1  28573  frgr3vlem1  28682  3vfriswmgrlem  28686  fzto1st  31415  psgnfzto1st  31417  wl-equsal1t  35744  ax12f  36996  incssnn0  40570  lzenom  40629  clsk1independent  41694  iidn3  42159  truniALT  42199  onfrALTlem2  42204  ee220  42296  dvmptfprodlem  43534  fourierdlem89  43785  fourierdlem91  43787  sge0reuz  44035  hoi2toco  44195  linds0  45864