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  2171  sbcrext  3661  oaordi  7784  nnaordi  7856  cantnfval2  8734  infxpenc2lem1  9046  ackbij1lem16  9263  sornom  9305  fin23lem36  9376  isf32lem1  9381  isf32lem2  9382  zornn0g  9533  canthwe  9679  indpi  9935  seqid2  13054  swrdccatin12lem3  13699  fsum2d  14710  fsumabs  14740  fsumiun  14760  fprod2d  14918  prmodvdslcmf  15958  prmlem1a  16020  gicsubgen  17928  dmatelnd  20520  dis2ndc  21484  1stcelcls  21485  ptcmpfi  21837  caubl  23325  caublcls  23326  volsuplem  23543  cpnord  23918  fsumvma  25159  gausslemma2dlem4  25315  pntpbnd1  25496  clwwlknonex2lem2  27284  3pthdlem1  27344  frgr3vlem1  27455  3vfriswmgrlem  27459  fzto1st  30193  psgnfzto1st  30195  wl-equsal1t  33661  ax12f  34746  incssnn0  37798  lzenom  37857  clsk1independent  38868  iidn3  39230  truniALT  39274  onfrALTlem2  39284  ee220  39386  dvmptfprodlem  40672  fourierdlem89  40924  fourierdlem91  40926  sge0reuz  41176  hoi2toco  41336  linds0  42777