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  2175  sbcrext  3819  mptexgf  7228  oaordi  8557  nnaordi  8630  mapsnend  9067  cantnfval2  9673  infxpenc2lem1  10101  ackbij1lem16  10315  sornom  10358  fin23lem36  10429  isf32lem1  10434  isf32lem2  10435  zornn0g  10586  canthwe  10739  indpi  10995  seqid2  14194  pfxccatin12lem3  14885  fsum2d  15942  fsumabs  15973  fsumiun  15993  fprod2d  16153  prmodvdslcmf  17230  prmlem1a  17289  gicsubgen  19498  dmatelnd  22816  dis2ndc  23784  1stcelcls  23785  ptcmpfi  24137  caubl  25634  caublcls  25635  volsuplem  25881  cpnord  26260  fsumvma  27545  gausslemma2dlem4  27701  pntpbnd1  27918  3pthdlem1  30770  frgr3vlem1  30879  3vfriswmgrlem  30883  fzto1st  33710  psgnfzto1st  33712  nmuladdss  37054  wl-equsal1t  38567  disjimeceqbi2  39832  ax12f  40090  incssnn0  43815  lzenom  43874  omabs2  44427  clsk1independent  45139  iidn3  45577  truniALT  45617  onfrALTlem2  45622  ee220  45714  dvmptfprodlem  47047  dvnprodlem1  47049  fourierdlem89  47298  fourierdlem91  47300  sge0reuz  47550  hoi2toco  47710  gpgedg2iv  49258  linds0  49670