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  2176  sbcrext  3820  mptexgf  7220  oaordi  8538  nnaordi  8611  mapsnend  9048  cantnfval2  9654  infxpenc2lem1  10079  ackbij1lem16  10293  sornom  10336  fin23lem36  10407  isf32lem1  10412  isf32lem2  10413  zornn0g  10564  canthwe  10717  indpi  10973  seqid2  14171  pfxccatin12lem3  14861  fsum2d  15917  fsumabs  15948  fsumiun  15968  fprod2d  16128  prmodvdslcmf  17205  prmlem1a  17264  gicsubgen  19473  dmatelnd  22791  dis2ndc  23759  1stcelcls  23760  ptcmpfi  24112  caubl  25609  caublcls  25610  volsuplem  25856  cpnord  26235  fsumvma  27522  gausslemma2dlem4  27678  pntpbnd1  27895  3pthdlem1  30747  frgr3vlem1  30856  3vfriswmgrlem  30860  fzto1st  33646  psgnfzto1st  33648  nmuladdss  36932  wl-equsal1t  38442  disjimeceqbi2  39707  ax12f  39965  incssnn0  43675  lzenom  43734  omabs2  44292  clsk1independent  45005  iidn3  45443  truniALT  45483  onfrALTlem2  45488  ee220  45580  dvmptfprodlem  46898  dvnprodlem1  46900  fourierdlem89  47149  fourierdlem91  47151  sge0reuz  47401  hoi2toco  47561  gpgedg2iv  49109  linds0  49521