Theorem 2a1i 12

Description: Inference introducing two antecedents. Two applications of a1i 11. Inference associated with 2a1 29. (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  2174  sbcrext  3827  mptexgf  7222  oaordi  8532  nnaordi  8605  mapsnend  9034  cantnfval2  9639  infxpenc2lem1  10004  ackbij1lem16  10218  sornom  10262  fin23lem36  10333  isf32lem1  10338  isf32lem2  10339  zornn0g  10490  canthwe  10637  indpi  10893  seqid2  14086  pfxccatin12lem3  14771  fsum2d  15824  fsumabs  15855  fsumiun  15875  fprod2d  16037  prmodvdslcmf  17108  prmlem1a  17167  gicsubgen  19350  dmatelnd  22634  dis2ndc  23598  1stcelcls  23599  ptcmpfi  23951  caubl  25448  caublcls  25449  volsuplem  25695  cpnord  26075  fsumvma  27355  gausslemma2dlem4  27511  pntpbnd1  27728  3pthdlem1  30493  frgr3vlem1  30602  3vfriswmgrlem  30606  fzto1st  33401  psgnfzto1st  33403  nmuladdss  36668  wl-equsal1t  38175  disjimeceqbi2  39434  ax12f  39692  incssnn0  43422  lzenom  43481  omabs2  44039  clsk1independent  44752  iidn3  45190  truniALT  45230  onfrALTlem2  45235  ee220  45327  dvmptfprodlem  46638  dvnprodlem1  46640  fourierdlem89  46889  fourierdlem91  46891  sge0reuz  47141  hoi2toco  47301  gpgedg2iv  48809  linds0  49222