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  2145  sbcrext  3812  mptexgf  7170  oaordi  8474  nnaordi  8547  mapsnend  8976  cantnfval2  9581  infxpenc2lem1  9932  ackbij1lem16  10147  sornom  10190  fin23lem36  10261  isf32lem1  10266  isf32lem2  10267  zornn0g  10418  canthwe  10565  indpi  10821  seqid2  14001  pfxccatin12lem3  14685  fsum2d  15724  fsumabs  15755  fsumiun  15775  fprod2d  15937  prmodvdslcmf  17009  prmlem1a  17068  gicsubgen  19245  dmatelnd  22471  dis2ndc  23435  1stcelcls  23436  ptcmpfi  23788  caubl  25285  caublcls  25286  volsuplem  25532  cpnord  25912  fsumvma  27190  gausslemma2dlem4  27346  pntpbnd1  27563  3pthdlem1  30249  frgr3vlem1  30358  3vfriswmgrlem  30362  fzto1st  33179  psgnfzto1st  33181  wl-equsal1t  37881  disjimeceqbi2  39142  ax12f  39400  incssnn0  43157  lzenom  43216  omabs2  43778  clsk1independent  44491  iidn3  44946  truniALT  44986  onfrALTlem2  44991  ee220  45083  dvmptfprodlem  46390  dvnprodlem1  46392  fourierdlem89  46641  fourierdlem91  46643  sge0reuz  46893  hoi2toco  47053  gpgedg2iv  48555  linds0  48953