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  3839  mptexgf  7199  oaordi  8513  nnaordi  8585  mapsnend  9010  cantnfval2  9629  infxpenc2lem1  9979  ackbij1lem16  10194  sornom  10237  fin23lem36  10308  isf32lem1  10313  isf32lem2  10314  zornn0g  10465  canthwe  10611  indpi  10867  seqid2  14020  pfxccatin12lem3  14704  fsum2d  15744  fsumabs  15774  fsumiun  15794  fprod2d  15954  prmodvdslcmf  17025  prmlem1a  17084  gicsubgen  19218  dmatelnd  22390  dis2ndc  23354  1stcelcls  23355  ptcmpfi  23707  caubl  25215  caublcls  25216  volsuplem  25463  cpnord  25844  fsumvma  27131  gausslemma2dlem4  27287  pntpbnd1  27504  3pthdlem1  30100  frgr3vlem1  30209  3vfriswmgrlem  30213  fzto1st  33067  psgnfzto1st  33069  wl-equsal1t  37537  ax12f  38940  incssnn0  42706  lzenom  42765  omabs2  43328  clsk1independent  44042  iidn3  44498  truniALT  44538  onfrALTlem2  44543  ee220  44635  dvmptfprodlem  45949  dvnprodlem1  45951  fourierdlem89  46200  fourierdlem91  46202  sge0reuz  46452  hoi2toco  46612  gpgedg2iv  48062  linds0  48458