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

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6

This theorem is referenced by:  ax13dgen3  2180  sbcrext  3835  mptexgf  7218  oaordi  8527  nnaordi  8600  mapsnend  9029  cantnfval2  9634  infxpenc2lem1  9999  ackbij1lem16  10213  sornom  10257  fin23lem36  10328  isf32lem1  10333  isf32lem2  10334  zornn0g  10485  canthwe  10632  indpi  10888  seqid2  14080  pfxccatin12lem3  14765  fsum2d  15818  fsumabs  15849  fsumiun  15869  fprod2d  16031  prmodvdslcmf  17103  prmlem1a  17162  gicsubgen  19345  dmatelnd  22618  dis2ndc  23582  1stcelcls  23583  ptcmpfi  23935  caubl  25432  caublcls  25433  volsuplem  25679  cpnord  26059  fsumvma  27339  gausslemma2dlem4  27495  pntpbnd1  27712  3pthdlem1  30452  frgr3vlem1  30561  3vfriswmgrlem  30565  fzto1st  33360  psgnfzto1st  33362  wl-equsal1t  38080  disjimeceqbi2  39341  ax12f  39599  incssnn0  43329  lzenom  43388  omabs2  43946  clsk1independent  44659  iidn3  45097  truniALT  45137  onfrALTlem2  45142  ee220  45234  dvmptfprodlem  46545  dvnprodlem1  46547  fourierdlem89  46796  fourierdlem91  46798  sge0reuz  47048  hoi2toco  47208  gpgedg2iv  48716  linds0  49125