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  2172  sbcrext  3826  mptexgf  7202  oaordi  8510  nnaordi  8583  mapsnend  9013  cantnfval2  9621  infxpenc2lem1  9972  ackbij1lem16  10187  sornom  10231  fin23lem36  10302  isf32lem1  10307  isf32lem2  10308  zornn0g  10459  canthwe  10606  indpi  10862  seqid2  14058  pfxccatin12lem3  14742  fsum2d  15781  fsumabs  15812  fsumiun  15832  fprod2d  15994  prmodvdslcmf  17066  prmlem1a  17125  gicsubgen  19302  dmatelnd  22536  dis2ndc  23500  1stcelcls  23501  ptcmpfi  23853  caubl  25350  caublcls  25351  volsuplem  25597  cpnord  25977  fsumvma  27254  gausslemma2dlem4  27410  pntpbnd1  27627  3pthdlem1  30312  frgr3vlem1  30421  3vfriswmgrlem  30425  fzto1st  33244  psgnfzto1st  33246  wl-equsal1t  38009  disjimeceqbi2  39270  ax12f  39528  incssnn0  43256  lzenom  43315  omabs2  43873  clsk1independent  44586  iidn3  45041  truniALT  45081  onfrALTlem2  45086  ee220  45178  dvmptfprodlem  46482  dvnprodlem1  46484  fourierdlem89  46733  fourierdlem91  46735  sge0reuz  46985  hoi2toco  47145  gpgedg2iv  48653  linds0  49051