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 ⊢ (𝜓 → (𝜒 → 𝜑))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6

This theorem is used by:  ax13dgen3  2176  sbcrext  3823  mptexgf  7225  oaordi  8537  nnaordi  8610  mapsnend  9047  cantnfval2  9652  infxpenc2lem1  10026  ackbij1lem16  10240  sornom  10283  fin23lem36  10354  isf32lem1  10359  isf32lem2  10360  zornn0g  10511  canthwe  10664  indpi  10920  seqid2  14116  pfxccatin12lem3  14805  fsum2d  15861  fsumabs  15892  fsumiun  15912  fprod2d  16074  prmodvdslcmf  17145  prmlem1a  17204  gicsubgen  19412  dmatelnd  22724  dis2ndc  23692  1stcelcls  23693  ptcmpfi  24045  caubl  25542  caublcls  25543  volsuplem  25789  cpnord  26169  fsumvma  27457  gausslemma2dlem4  27613  pntpbnd1  27830  3pthdlem1  30652  frgr3vlem1  30761  3vfriswmgrlem  30765  fzto1st  33551  psgnfzto1st  33553  nmuladdss  36801  wl-equsal1t  38313  disjimeceqbi2  39563  ax12f  39821  incssnn0  43564  lzenom  43623  omabs2  44181  clsk1independent  44894  iidn3  45332  truniALT  45372  onfrALTlem2  45377  ee220  45469  dvmptfprodlem  46780  dvnprodlem1  46782  fourierdlem89  47031  fourierdlem91  47033  sge0reuz  47283  hoi2toco  47443  gpgedg2iv  48991  linds0  49403