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  2140  sbcrext  3836  mptexgf  7196  oaordi  8510  nnaordi  8582  mapsnend  9007  cantnfval2  9622  infxpenc2lem1  9972  ackbij1lem16  10187  sornom  10230  fin23lem36  10301  isf32lem1  10306  isf32lem2  10307  zornn0g  10458  canthwe  10604  indpi  10860  seqid2  14013  pfxccatin12lem3  14697  fsum2d  15737  fsumabs  15767  fsumiun  15787  fprod2d  15947  prmodvdslcmf  17018  prmlem1a  17077  gicsubgen  19211  dmatelnd  22383  dis2ndc  23347  1stcelcls  23348  ptcmpfi  23700  caubl  25208  caublcls  25209  volsuplem  25456  cpnord  25837  fsumvma  27124  gausslemma2dlem4  27280  pntpbnd1  27497  3pthdlem1  30093  frgr3vlem1  30202  3vfriswmgrlem  30206  fzto1st  33060  psgnfzto1st  33062  wl-equsal1t  37530  ax12f  38933  incssnn0  42699  lzenom  42758  omabs2  43321  clsk1independent  44035  iidn3  44491  truniALT  44531  onfrALTlem2  44536  ee220  44628  dvmptfprodlem  45942  dvnprodlem1  45944  fourierdlem89  46193  fourierdlem91  46195  sge0reuz  46445  hoi2toco  46605  gpgedg2iv  48058  linds0  48454