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  2137  sbcrext  3882  mptexgf  7242  oaordi  8583  nnaordi  8655  mapsnend  9075  cantnfval2  9707  infxpenc2lem1  10057  ackbij1lem16  10272  sornom  10315  fin23lem36  10386  isf32lem1  10391  isf32lem2  10392  zornn0g  10543  canthwe  10689  indpi  10945  seqid2  14086  pfxccatin12lem3  14767  fsum2d  15804  fsumabs  15834  fsumiun  15854  fprod2d  16014  prmodvdslcmf  17081  prmlem1a  17141  gicsubgen  19310  dmatelnd  22518  dis2ndc  23484  1stcelcls  23485  ptcmpfi  23837  caubl  25356  caublcls  25357  volsuplem  25604  cpnord  25986  fsumvma  27272  gausslemma2dlem4  27428  pntpbnd1  27645  3pthdlem1  30193  frgr3vlem1  30302  3vfriswmgrlem  30306  fzto1st  33106  psgnfzto1st  33108  wl-equsal1t  37523  ax12f  38922  incssnn0  42699  lzenom  42758  omabs2  43322  clsk1independent  44036  iidn3  44499  truniALT  44539  onfrALTlem2  44544  ee220  44636  dvmptfprodlem  45900  dvnprodlem1  45902  fourierdlem89  46151  fourierdlem91  46153  sge0reuz  46403  hoi2toco  46563  linds0  48311