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  2178  sbcrext  3824  mptexgf  7251  oaordi  8582  nnaordi  8655  mapsnend  9092  cantnfval2  9697  infxpenc2lem1  10125  ackbij1lem16  10339  sornom  10382  fin23lem36  10453  isf32lem1  10458  isf32lem2  10459  zornn0g  10610  canthwe  10763  indpi  11019  seqid2  14218  pfxccatin12lem3  14909  fsum2d  15966  fsumabs  15997  fsumiun  16017  fprod2d  16177  prmodvdslcmf  17254  prmlem1a  17313  gicsubgen  19523  dmatelnd  22841  dis2ndc  23809  1stcelcls  23810  ptcmpfi  24162  caubl  25659  caublcls  25660  volsuplem  25906  cpnord  26285  fsumvma  27570  gausslemma2dlem4  27726  pntpbnd1  27943  3pthdlem1  30795  frgr3vlem1  30904  3vfriswmgrlem  30908  fzto1st  33734  psgnfzto1st  33736  nmuladdss  37140  wl-equsal1t  38666  disjimeceqbi2  39931  ax12f  40189  incssnn0  43915  lzenom  43974  omabs2  44526  clsk1independent  45238  iidn3  45675  truniALT  45715  onfrALTlem2  45720  ee220  45812  dvmptfprodlem  47159  dvnprodlem1  47161  fourierdlem89  47410  fourierdlem91  47412  sge0reuz  47662  hoi2toco  47822  gpgedg2iv  49370  linds0  49782