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  2177  sbcrext  3829  mptexgf  7227  oaordi  8540  nnaordi  8613  mapsnend  9043  cantnfval2  9648  infxpenc2lem1  10022  ackbij1lem16  10236  sornom  10279  fin23lem36  10350  isf32lem1  10355  isf32lem2  10356  zornn0g  10507  canthwe  10654  indpi  10910  seqid2  14104  pfxccatin12lem3  14793  fsum2d  15848  fsumabs  15879  fsumiun  15899  fprod2d  16061  prmodvdslcmf  17132  prmlem1a  17191  gicsubgen  19380  dmatelnd  22690  dis2ndc  23654  1stcelcls  23655  ptcmpfi  24007  caubl  25504  caublcls  25505  volsuplem  25751  cpnord  26131  fsumvma  27414  gausslemma2dlem4  27570  pntpbnd1  27787  3pthdlem1  30552  frgr3vlem1  30661  3vfriswmgrlem  30665  fzto1st  33454  psgnfzto1st  33456  nmuladdss  36726  wl-equsal1t  38238  disjimeceqbi2  39497  ax12f  39755  incssnn0  43483  lzenom  43542  omabs2  44100  clsk1independent  44813  iidn3  45251  truniALT  45291  onfrALTlem2  45296  ee220  45388  dvmptfprodlem  46699  dvnprodlem1  46701  fourierdlem89  46950  fourierdlem91  46952  sge0reuz  47202  hoi2toco  47362  gpgedg2iv  48873  linds0  49286