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  2139  sbcrext  3895  mptexgf  7259  oaordi  8602  nnaordi  8674  mapsnend  9101  cantnfval2  9738  infxpenc2lem1  10088  ackbij1lem16  10303  sornom  10346  fin23lem36  10417  isf32lem1  10422  isf32lem2  10423  zornn0g  10574  canthwe  10720  indpi  10976  seqid2  14099  pfxccatin12lem3  14780  fsum2d  15819  fsumabs  15849  fsumiun  15869  fprod2d  16029  prmodvdslcmf  17094  prmlem1a  17154  gicsubgen  19319  dmatelnd  22523  dis2ndc  23489  1stcelcls  23490  ptcmpfi  23842  caubl  25361  caublcls  25362  volsuplem  25609  cpnord  25991  fsumvma  27275  gausslemma2dlem4  27431  pntpbnd1  27648  3pthdlem1  30196  frgr3vlem1  30305  3vfriswmgrlem  30309  fzto1st  33096  psgnfzto1st  33098  wl-equsal1t  37496  ax12f  38896  incssnn0  42667  lzenom  42726  omabs2  43294  clsk1independent  44008  iidn3  44472  truniALT  44512  onfrALTlem2  44517  ee220  44609  dvmptfprodlem  45865  fourierdlem89  46116  fourierdlem91  46118  sge0reuz  46368  hoi2toco  46528  linds0  48194