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  2181  sbcrext  3670  oaordi  7831  nnaordi  7903  cantnfval2  8781  infxpenc2lem1  9093  ackbij1lem16  9310  sornom  9352  fin23lem36  9423  isf32lem1  9428  isf32lem2  9429  zornn0g  9580  canthwe  9726  indpi  9982  seqid2  13054  swrdccatin12lem3  13738  fsum2d  14787  fsumabs  14817  fsumiun  14837  fprod2d  14994  prmodvdslcmf  16030  prmlem1a  16087  gicsubgen  17984  dmatelnd  20579  dis2ndc  21543  1stcelcls  21544  ptcmpfi  21896  caubl  23385  caublcls  23386  volsuplem  23613  cpnord  23989  fsumvma  25229  gausslemma2dlem4  25385  pntpbnd1  25566  clwwlknonex2lem2  27382  3pthdlem1  27442  frgr3vlem1  27553  3vfriswmgrlem  27557  fzto1st  30300  psgnfzto1st  30302  wl-equsal1t  33752  ax12f  34896  incssnn0  37952  lzenom  38011  clsk1independent  39018  iidn3  39379  truniALT  39419  onfrALTlem2  39424  ee220  39525  dvmptfprodlem  40797  fourierdlem89  41049  fourierdlem91  41051  sge0reuz  41301  hoi2toco  41461  linds0  42923