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  2140  sbcrext  3827  mptexgf  7162  oaordi  8471  nnaordi  8543  mapsnend  8968  cantnfval2  9584  infxpenc2lem1  9932  ackbij1lem16  10147  sornom  10190  fin23lem36  10261  isf32lem1  10266  isf32lem2  10267  zornn0g  10418  canthwe  10564  indpi  10820  seqid2  13973  pfxccatin12lem3  14656  fsum2d  15696  fsumabs  15726  fsumiun  15746  fprod2d  15906  prmodvdslcmf  16977  prmlem1a  17036  gicsubgen  19176  dmatelnd  22399  dis2ndc  23363  1stcelcls  23364  ptcmpfi  23716  caubl  25224  caublcls  25225  volsuplem  25472  cpnord  25853  fsumvma  27140  gausslemma2dlem4  27296  pntpbnd1  27513  3pthdlem1  30126  frgr3vlem1  30235  3vfriswmgrlem  30239  fzto1st  33058  psgnfzto1st  33060  wl-equsal1t  37515  ax12f  38918  incssnn0  42684  lzenom  42743  omabs2  43305  clsk1independent  44019  iidn3  44475  truniALT  44515  onfrALTlem2  44520  ee220  44612  dvmptfprodlem  45926  dvnprodlem1  45928  fourierdlem89  46177  fourierdlem91  46179  sge0reuz  46429  hoi2toco  46589  gpgedg2iv  48052  linds0  48451