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  2145  sbcrext  3825  mptexgf  7178  oaordi  8483  nnaordi  8556  mapsnend  8985  cantnfval2  9590  infxpenc2lem1  9941  ackbij1lem16  10156  sornom  10199  fin23lem36  10270  isf32lem1  10275  isf32lem2  10276  zornn0g  10427  canthwe  10574  indpi  10830  seqid2  13983  pfxccatin12lem3  14667  fsum2d  15706  fsumabs  15736  fsumiun  15756  fprod2d  15916  prmodvdslcmf  16987  prmlem1a  17046  gicsubgen  19220  dmatelnd  22452  dis2ndc  23416  1stcelcls  23417  ptcmpfi  23769  caubl  25276  caublcls  25277  volsuplem  25524  cpnord  25905  fsumvma  27192  gausslemma2dlem4  27348  pntpbnd1  27565  3pthdlem1  30251  frgr3vlem1  30360  3vfriswmgrlem  30364  fzto1st  33196  psgnfzto1st  33198  wl-equsal1t  37791  disjimeceqbi2  39052  ax12f  39310  incssnn0  43062  lzenom  43121  omabs2  43683  clsk1independent  44396  iidn3  44851  truniALT  44891  onfrALTlem2  44896  ee220  44988  dvmptfprodlem  46296  dvnprodlem1  46298  fourierdlem89  46547  fourierdlem91  46549  sge0reuz  46799  hoi2toco  46959  gpgedg2iv  48421  linds0  48819