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  2176  sbcrext  3829  mptexgf  7210  oaordi  8519  nnaordi  8592  mapsnend  9021  cantnfval2  9626  infxpenc2lem1  9991  ackbij1lem16  10205  sornom  10249  fin23lem36  10320  isf32lem1  10325  isf32lem2  10326  zornn0g  10477  canthwe  10624  indpi  10880  seqid2  14075  pfxccatin12lem3  14759  fsum2d  15812  fsumabs  15843  fsumiun  15863  fprod2d  16025  prmodvdslcmf  17097  prmlem1a  17156  gicsubgen  19340  dmatelnd  22614  dis2ndc  23578  1stcelcls  23579  ptcmpfi  23931  caubl  25428  caublcls  25429  volsuplem  25675  cpnord  26055  fsumvma  27335  gausslemma2dlem4  27491  pntpbnd1  27708  3pthdlem1  30424  frgr3vlem1  30533  3vfriswmgrlem  30537  fzto1st  33336  psgnfzto1st  33338  wl-equsal1t  38057  disjimeceqbi2  39318  ax12f  39576  incssnn0  43304  lzenom  43363  omabs2  43921  clsk1independent  44634  iidn3  45075  truniALT  45115  onfrALTlem2  45120  ee220  45212  dvmptfprodlem  46516  dvnprodlem1  46518  fourierdlem89  46767  fourierdlem91  46769  sge0reuz  47019  hoi2toco  47179  gpgedg2iv  48687  linds0  49096